diff -r 253f6808dabe -r ef59550a55d3 src/ZF/UNITY/Constrains.thy
--- a/src/ZF/UNITY/Constrains.thy	Thu Jul 23 18:44:08 2009 +0200
+++ b/src/ZF/UNITY/Constrains.thy	Thu Jul 23 18:44:09 2009 +0200
@@ -471,7 +471,7 @@
 (*proves "co" properties when the program is specified*)
 
 fun constrains_tac ctxt =
-  let val css as (cs, ss) = local_clasimpset_of ctxt in
+  let val css as (cs, ss) = clasimpset_of ctxt in
    SELECT_GOAL
       (EVERY [REPEAT (Always_Int_tac 1),
               REPEAT (etac @{thm Always_ConstrainsI} 1
@@ -494,7 +494,7 @@
 
 (*For proving invariants*)
 fun always_tac ctxt i = 
-    rtac @{thm AlwaysI} i THEN force_tac (local_clasimpset_of ctxt) i THEN constrains_tac ctxt i;
+    rtac @{thm AlwaysI} i THEN force_tac (clasimpset_of ctxt) i THEN constrains_tac ctxt i;
 *}
 
 setup Program_Defs.setup