src/HOLCF/IOA/meta_theory/Traces.ML

--- a/src/HOLCF/IOA/meta_theory/Traces.ML	Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Mon Nov 03 14:06:27 1997 +0100
@@ -23,15 +23,15 @@
 
 
 goal thy  "filter_act`UU = UU";
-by (simp_tac (!simpset addsimps [filter_act_def]) 1);
+by (simp_tac (simpset() addsimps [filter_act_def]) 1);
 qed"filter_act_UU";
 
 goal thy  "filter_act`nil = nil";
-by (simp_tac (!simpset addsimps [filter_act_def]) 1);
+by (simp_tac (simpset() addsimps [filter_act_def]) 1);
 qed"filter_act_nil";
 
 goal thy "filter_act`(x>>xs) = (fst x) >> filter_act`xs";
-by (simp_tac (!simpset addsimps [filter_act_def]) 1);
+by (simp_tac (simpset() addsimps [filter_act_def]) 1);
 qed"filter_act_cons";
 
 Addsimps [filter_act_UU,filter_act_nil,filter_act_cons];
@@ -42,11 +42,11 @@
 (* ---------------------------------------------------------------- *)
 
 goal thy "mk_trace A`UU=UU";
-by (simp_tac (!simpset addsimps [mk_trace_def]) 1);
+by (simp_tac (simpset() addsimps [mk_trace_def]) 1);
 qed"mk_trace_UU";
 
 goal thy "mk_trace A`nil=nil";
-by (simp_tac (!simpset addsimps [mk_trace_def]) 1);
+by (simp_tac (simpset() addsimps [mk_trace_def]) 1);
 qed"mk_trace_nil";
 
 goal thy "mk_trace A`(at >> xs) =    \
@@ -54,7 +54,7 @@
 \                 then (fst at) >> (mk_trace A`xs) \   
 \                 else mk_trace A`xs)";
 
-by (asm_full_simp_tac (!simpset addsimps [mk_trace_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [mk_trace_def]) 1);
 qed"mk_trace_cons";
 
 Addsimps [mk_trace_UU,mk_trace_nil,mk_trace_cons];
@@ -74,7 +74,7 @@
 by (rtac fix_eq2 1);
 by (rtac is_exec_fragC_def 1);
 by (rtac beta_cfun 1);
-by (simp_tac (!simpset addsimps [flift1_def]) 1);
+by (simp_tac (simpset() addsimps [flift1_def]) 1);
 qed"is_exec_fragC_unfold";
 
 goal thy "(is_exec_fragC A`UU) s=UU";
@@ -92,7 +92,7 @@
 \                andalso (is_exec_fragC A`xs)(snd pr))";
 by (rtac trans 1);
 by (stac is_exec_fragC_unfold 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
 by (Simp_tac 1);
 qed"is_exec_fragC_cons";
 
@@ -105,17 +105,17 @@
 (* ---------------------------------------------------------------- *)
 
 goal thy "is_exec_frag A (s, UU)";
-by (simp_tac (!simpset addsimps [is_exec_frag_def]) 1);
+by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1);
 qed"is_exec_frag_UU";
 
 goal thy "is_exec_frag A (s, nil)";
-by (simp_tac (!simpset addsimps [is_exec_frag_def]) 1);
+by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1);
 qed"is_exec_frag_nil";
 
 goal thy "is_exec_frag A (s, (a,t)>>ex) = \
 \                               (((s,a,t):trans_of A) & \
 \                               is_exec_frag A (t, ex))";
-by (simp_tac (!simpset addsimps [is_exec_frag_def]) 1);
+by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1);
 qed"is_exec_frag_cons";
 
 
@@ -169,14 +169,14 @@
 (* main case *)
 ren "ss a t" 1;
 by (safe_tac set_cs);
-by (REPEAT (asm_full_simp_tac (!simpset addsimps [is_trans_of_def]) 1));
+by (REPEAT (asm_full_simp_tac (simpset() addsimps [is_trans_of_def]) 1));
 qed"execfrag_in_sig";
 
 goal thy 
   "!! A.[|  is_trans_of A; x:executions A |] ==> \
 \ Forall (%a. a:act A) (filter_act`(snd x))";
 
-by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
 by (pair_tac "x" 1);
 by (rtac (execfrag_in_sig RS spec RS mp) 1);
 by (Auto_tac());
@@ -186,7 +186,7 @@
   "!! A.[|  is_trans_of A; x:schedules A |] ==> \
 \   Forall (%a. a:act A) x";
 
-by (fast_tac (!claset addSIs [exec_in_sig]) 1);
+by (fast_tac (claset() addSIs [exec_in_sig]) 1);
 qed"scheds_in_sig";