
diff -r 741deccec4e3 -r bca33c49b083 src/ZF/UNITY/ClientImpl.thy
--- a/src/ZF/UNITY/ClientImpl.thy	Sat Mar 26 18:20:29 2005 +0100
+++ b/src/ZF/UNITY/ClientImpl.thy	Mon Mar 28 16:19:56 2005 +0200
@@ -9,13 +9,6 @@
 
 theory ClientImpl = AllocBase + Guar:
 
-(*move to Constrains.thy when the latter is converted to Isar format*)
-method_setup constrains = {*
-    Method.ctxt_args (fn ctxt =>
-        Method.METHOD (fn facts =>
-            gen_constrains_tac (local_clasimpset_of ctxt) 1)) *}
-    "for proving safety properties"
-
 consts
   ask :: i (* input history:  tokens requested *)
   giv :: i (* output history: tokens granted *)




