changeset 27882 | eaa9fef9f4c1 |
parent 27239 | f2f42f9fa09d |
child 30549 | d2d7874648bd |
--- a/src/ZF/UNITY/SubstAx.thy Thu Aug 14 21:06:07 2008 +0200 +++ b/src/ZF/UNITY/SubstAx.thy Fri Aug 15 15:50:44 2008 +0200 @@ -378,7 +378,7 @@ method_setup ensures_tac = {* fn args => fn ctxt => - Method.goal_args' (Scan.lift Args.name) (ensures_tac ctxt) + Method.goal_args' (Scan.lift Args.name_source) (ensures_tac ctxt) args ctxt *} "for proving progress properties"