--- 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