src/HOL/TLA/Action.ML
changeset 4089 96fba19bcbe2
parent 3945 ae9c61d69888
child 4477 b3e5857d8d99
     1.1 --- a/src/HOL/TLA/Action.ML	Mon Nov 03 12:12:10 1997 +0100
     1.2 +++ b/src/HOL/TLA/Action.ML	Mon Nov 03 12:13:18 1997 +0100
     1.3 @@ -56,7 +56,7 @@
     1.4                    handle _ => int_unlift th)
     1.5         | _ => th);
     1.6  
     1.7 -simpset := !simpset setmksimps ((mksimps mksimps_pairs) o maybe_unlift);
     1.8 +simpset_ref() := simpset() setmksimps ((mksimps mksimps_pairs) o maybe_unlift);
     1.9  
    1.10  (* make act_rews be always active -- intensional_rews has been added before *)
    1.11  Addsimps act_rews;
    1.12 @@ -75,7 +75,7 @@
    1.13  		      ORELSE' (eresolve_tac (elims @ [conjE,disjE,exE_prop]))))
    1.14           i);
    1.15  (* default version without additional plug-in rules *)
    1.16 -fun Action_simp_tac i = (action_simp_tac (!simpset) [] [] i);
    1.17 +fun Action_simp_tac i = (action_simp_tac (simpset()) [] [] i);
    1.18  
    1.19  
    1.20  (* ==================== Simplification of abstractions ==================== *)