--- a/src/HOL/UNITY/UNITY_Main.thy Wed Nov 29 15:44:46 2006 +0100
+++ b/src/HOL/UNITY/UNITY_Main.thy Wed Nov 29 15:44:51 2006 +0100
@@ -11,13 +11,12 @@
method_setup safety = {*
Method.ctxt_args (fn ctxt =>
- Method.METHOD (fn facts =>
- gen_constrains_tac (local_clasimpset_of ctxt) 1)) *}
+ Method.SIMPLE_METHOD' (gen_constrains_tac (local_clasimpset_of ctxt))) *}
"for proving safety properties"
method_setup ensures_tac = {*
fn args => fn ctxt =>
- Method.goal_args' (Scan.lift Args.name)
+ Method.goal_args' (Scan.lift Args.name)
(gen_ensures_tac (local_clasimpset_of ctxt))
args ctxt *}
"for proving progress properties"