diff -r f0d543629376 -r eaa9fef9f4c1 src/HOL/UNITY/UNITY_Main.thy --- a/src/HOL/UNITY/UNITY_Main.thy Thu Aug 14 21:06:07 2008 +0200 +++ b/src/HOL/UNITY/UNITY_Main.thy Fri Aug 15 15:50:44 2008 +0200 @@ -16,7 +16,7 @@ method_setup ensures_tac = {* fn args => fn ctxt => - Method.goal_args' (Scan.lift Args.name) + Method.goal_args' (Scan.lift Args.name_source) (ensures_tac (local_clasimpset_of ctxt)) args ctxt *} "for proving progress properties"