Removed admits from the definition of [do_regularize].

They will have to be in the implementations of Level.Intf, but that's more
acceptable (I think).
one less admit