src/ZF/UNITY/SubstAx.thy

                         ALLGOALS (clarify_tac ctxt),
             ALLGOALS (asm_lr_simp_tac ss)])
   end;
 *}
 
-method_setup ensures_tac = {*
+method_setup ensures = {*
     Args.goal_spec -- Scan.lift Args.name_source >>
     (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
 *} "for proving progress properties"
 
 end