diff -r 726dc9146bb1 -r 02aed07e01bf src/HOL/UNITY/UNITY_Main.thy
--- a/src/HOL/UNITY/UNITY_Main.thy	Fri Jul 09 16:33:20 2004 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy	Sun Jul 11 20:33:22 2004 +0200
@@ -12,15 +12,13 @@
 method_setup constrains = {*
     Method.ctxt_args (fn ctxt =>
         Method.METHOD (fn facts => 
-            gen_constrains_tac (Classical.get_local_claset ctxt,
-                               Simplifier.get_local_simpset ctxt) 1)) *}
+            gen_constrains_tac (local_clasimpset_of ctxt) 1)) *}
     "for proving safety properties"
 
 method_setup ensures_tac = {*
     fn args => fn ctxt =>
         Method.goal_args' (Scan.lift Args.name) 
-           (gen_ensures_tac (Classical.get_local_claset ctxt,
-                               Simplifier.get_local_simpset ctxt))
+           (gen_ensures_tac (local_clasimpset_of ctxt))
            args ctxt *}
     "for proving progress properties"