1.1 --- a/src/ZF/UNITY/Constrains.thy	Fri May 13 16:03:03 2011 +0200
     1.2 +++ b/src/ZF/UNITY/Constrains.thy	Fri May 13 22:55:00 2011 +0200
     1.3 @@ -471,7 +471,7 @@
     1.4  (*proves "co" properties when the program is specified*)
     1.5  
     1.6  fun constrains_tac ctxt =
     1.7 -  let val css as (cs, ss) = clasimpset_of ctxt in
     1.8 +  let val ss = simpset_of ctxt in
     1.9     SELECT_GOAL
    1.10        (EVERY [REPEAT (Always_Int_tac 1),
    1.11                REPEAT (etac @{thm Always_ConstrainsI} 1
    1.12 @@ -481,20 +481,20 @@
    1.13                rtac @{thm constrainsI} 1,
    1.14                (* Three subgoals *)
    1.15                rewrite_goal_tac [@{thm st_set_def}] 3,
    1.16 -              REPEAT (force_tac css 2),
    1.17 +              REPEAT (force_tac ctxt 2),
    1.18                full_simp_tac (ss addsimps (Program_Defs.get ctxt)) 1,
    1.19 -              ALLGOALS (clarify_tac cs),
    1.20 +              ALLGOALS (clarify_tac ctxt),
    1.21                REPEAT (FIRSTGOAL (etac @{thm disjE})),
    1.22 -              ALLGOALS (clarify_tac cs),
    1.23 +              ALLGOALS (clarify_tac ctxt),
    1.24                REPEAT (FIRSTGOAL (etac @{thm disjE})),
    1.25 -              ALLGOALS (clarify_tac cs),
    1.26 +              ALLGOALS (clarify_tac ctxt),
    1.27                ALLGOALS (asm_full_simp_tac ss),
    1.28 -              ALLGOALS (clarify_tac cs)])
    1.29 +              ALLGOALS (clarify_tac ctxt)])
    1.30    end;
    1.31  
    1.32  (*For proving invariants*)
    1.33 -fun always_tac ctxt i = 
    1.34 -    rtac @{thm AlwaysI} i THEN force_tac (clasimpset_of ctxt) i THEN constrains_tac ctxt i;
    1.35 +fun always_tac ctxt i =
    1.36 +    rtac @{thm AlwaysI} i THEN force_tac ctxt i THEN constrains_tac ctxt i;
    1.37  *}
    1.38  
    1.39  setup Program_Defs.setup