src/HOL/MiniML/Instance.ML

--- a/src/HOL/MiniML/Instance.ML	Mon Nov 03 12:12:10 1997 +0100
+++ b/src/HOL/MiniML/Instance.ML	Mon Nov 03 12:13:18 1997 +0100
@@ -50,7 +50,7 @@
 \         (? S. !x:bound_tv sch. B x = mk_scheme (S x))";
 by (type_scheme.induct_tac "sch" 1);
 by (Simp_tac 1);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
 by (rtac exI 1);
 by (rtac ballI 1);
 by (rtac sym 1);
@@ -62,12 +62,12 @@
 by (dtac sym 1);
 by (dtac sym 1);
 by (REPEAT ((dtac mp 1) THEN (Fast_tac 1)));
-by (safe_tac (!claset));
+by (safe_tac (claset()));
 by (rename_tac "S1 S2" 1);
 by (res_inst_tac [("x","%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x)")] exI 1);
-by (safe_tac (!claset));
-by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
-by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
+by (safe_tac (claset()));
+by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
 by (strip_tac 1);
 by (dres_inst_tac [("x","x")] bspec 1);
 by (assume_tac 1);
@@ -82,8 +82,8 @@
 goal thy "!!sch. new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \
 \                                                 (bound_typ_inst (%k. TVar (k + n)) sch) = sch";
 by (type_scheme.induct_tac "sch" 1);
-by (simp_tac (!simpset addsimps [leD] addsplits [expand_if]) 1);
-by (simp_tac (!simpset addsimps [le_add2,diff_add_inverse2] addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsimps [leD] addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsimps [le_add2,diff_add_inverse2] addsplits [expand_if]) 1);
 by (Asm_simp_tac 1);
 qed_spec_mp "subst_to_scheme_inverse";
 
@@ -96,9 +96,9 @@
 \        (subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \
 \                         bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch)";
 by (type_scheme.induct_tac "sch" 1);
-by (simp_tac (!simpset addsplits [expand_if] addsimps [leD]) 1);
+by (simp_tac (simpset() addsplits [expand_if] addsimps [leD]) 1);
 by (Asm_simp_tac 1);
-by (asm_full_simp_tac (!simpset addsplits [expand_if] addsimps [leD]) 1);
+by (asm_full_simp_tac (simpset() addsplits [expand_if] addsimps [leD]) 1);
 val aux2 = result () RS mp;
 
 
@@ -120,10 +120,10 @@
 by (etac exE 1);
 by (REPEAT (etac conjE 1));
 by (dres_inst_tac [("n","n")] aux 1);
-by (asm_full_simp_tac (!simpset addsimps [subst_to_scheme_inverse]) 1);
+by (asm_full_simp_tac (simpset() addsimps [subst_to_scheme_inverse]) 1);
 by (res_inst_tac [("x","(subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S")] exI 1);
-by (asm_simp_tac (!simpset addsimps [aux2]) 1);
-by (safe_tac (!claset));
+by (asm_simp_tac (simpset() addsimps [aux2]) 1);
+by (safe_tac (claset()));
 by (res_inst_tac [("x","%n. bound_typ_inst S (B n)")] exI 1);
 by (type_scheme.induct_tac "sch" 1);
 by (Simp_tac 1);
@@ -132,7 +132,7 @@
 qed "le_type_scheme_def2";
 
 goalw thy [is_bound_typ_instance] "(mk_scheme t) <= sch = t <| sch";
-by (simp_tac (!simpset addsimps [le_type_scheme_def2]) 1); 
+by (simp_tac (simpset() addsimps [le_type_scheme_def2]) 1); 
 by (rtac iffI 1); 
 by (etac exE 1); 
 by (forward_tac [bound_scheme_inst_type] 1);
@@ -162,7 +162,7 @@
   "(sch # A <= sch' # B) = (sch <= (sch'::type_scheme) & A <= B)";
 by (Simp_tac 1);
 by (rtac iffI 1);
- by (SELECT_GOAL(safe_tac (!claset))1);
+ by (SELECT_GOAL(safe_tac (claset()))1);
   by (eres_inst_tac [("x","0")] allE 1);
   by (Asm_full_simp_tac 1);
  by (eres_inst_tac [("x","Suc i")] allE 1);
@@ -184,15 +184,15 @@
 qed "is_bound_typ_instance_closed_subst";
 
 goal thy "!!(sch::type_scheme) sch'. sch' <= sch ==> $S sch' <= $ S sch";
-by (asm_full_simp_tac (!simpset addsimps [le_type_scheme_def2]) 1);
+by (asm_full_simp_tac (simpset() addsimps [le_type_scheme_def2]) 1);
 by (etac exE 1);
-by (asm_full_simp_tac (!simpset addsimps [substitution_lemma]) 1);
+by (asm_full_simp_tac (simpset() addsimps [substitution_lemma]) 1);
 by (Fast_tac 1);
 qed "S_compatible_le_scheme";
 
 goalw thy [le_env_def,app_subst_list] "!!(A::type_scheme list) A'. A' <= A ==> $S A' <= $ S A";
-by (simp_tac (!simpset addcongs [conj_cong]) 1);
-by (fast_tac (!claset addSIs [S_compatible_le_scheme]) 1);
+by (simp_tac (simpset() addcongs [conj_cong]) 1);
+by (fast_tac (claset() addSIs [S_compatible_le_scheme]) 1);
 qed "S_compatible_le_scheme_lists";
 
 goalw thy [le_type_scheme_def] "!!t.[| t <| sch; sch <= sch' |] ==> t <| sch'";
@@ -220,7 +220,7 @@
 by (type_scheme.induct_tac "sch" 1);
   by (Simp_tac 1);
  by (Simp_tac 1);
- by (SELECT_GOAL(safe_tac(!claset))1);
+ by (SELECT_GOAL(safe_tac(claset()))1);
  by (eres_inst_tac [("x","TVar n -> TVar n")] allE 1);
  by (Asm_full_simp_tac 1);
  by (Fast_tac 1);
@@ -248,7 +248,7 @@
 
 goalw thy [le_type_scheme_def,is_bound_typ_instance]
   "!!sch1. (sch1 =-> sch2 <= sch1' =-> sch2') ==> sch1 <= sch1' & sch2 <= sch2'";
-by (fast_tac (!claset addss !simpset) 1);
+by (fast_tac (claset() addss simpset()) 1);
 qed "Fun_le_FunD";
 
 goal thy "(sch' <= sch1 =-> sch2) --> (? sch'1 sch'2. sch' = sch'1 =-> sch'2)";
@@ -285,7 +285,7 @@
  by (Simp_tac 1);
 by (rtac allI 1);
 by (list.induct_tac "A" 1);
- by (simp_tac (!simpset addsimps [le_env_def]) 1);
+ by (simp_tac (simpset() addsimps [le_env_def]) 1);
 by (Simp_tac 1);
-by (fast_tac (!claset addDs [le_type_scheme_free_tv]) 1);
+by (fast_tac (claset() addDs [le_type_scheme_free_tv]) 1);
 qed_spec_mp "le_env_free_tv";