src/HOL/MiniML/MiniML.ML

--- a/src/HOL/MiniML/MiniML.ML	Mon Nov 03 12:12:10 1997 +0100
+++ b/src/HOL/MiniML/MiniML.ML	Mon Nov 03 12:13:18 1997 +0100
@@ -12,14 +12,14 @@
 
 goal thy "!!t::typ. $(%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) t = $S t";
 by (rtac typ_substitutions_only_on_free_variables 1);
-by (asm_full_simp_tac (!simpset addsimps [Ball_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Ball_def]) 1);
 qed "s'_t_equals_s_t";
 
 Addsimps [s'_t_equals_s_t];
 
 goal thy "!!A::type_scheme list. $(%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) A = $S A";
 by (rtac scheme_list_substitutions_only_on_free_variables 1);
-by (asm_full_simp_tac (!simpset addsimps [Ball_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Ball_def]) 1);
 qed "s'_a_equals_s_a";
 
 Addsimps [s'_a_equals_s_a];
@@ -37,7 +37,7 @@
 
 goal thy "!!A::type_scheme list. $ (%x. TVar (if x : free_tv A then x else n + x)) A = $ id_subst A";
 by (rtac scheme_list_substitutions_only_on_free_variables 1);
-by (asm_full_simp_tac (!simpset addsimps [id_subst_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [id_subst_def]) 1);
 qed "alpha_A'";
 
 goal thy "!!A::type_scheme list. $ (%x. TVar (if x : free_tv A then x else n + x)) A = A";
@@ -82,7 +82,7 @@
 goalw thy [free_tv_subst,dom_def]
           "!!A. dom (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
 \               free_tv A Un free_tv t";
-by (simp_tac (!simpset addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsplits [expand_if]) 1);
 by (Fast_tac 1);
 qed "dom_S'";
 
@@ -95,7 +95,7 @@
 by (dtac (dom_S' RS subsetD) 1);
 by (rotate_tac 1 1);
 by (Asm_full_simp_tac 1);
-by (fast_tac (!claset addDs [free_tv_of_substitutions_extend_to_scheme_lists] 
+by (fast_tac (claset() addDs [free_tv_of_substitutions_extend_to_scheme_lists] 
                       addIs [free_tv_of_substitutions_extend_to_types RS subsetD]) 1);
 qed "cod_S'";
 
@@ -103,14 +103,14 @@
           "!!(A::type_scheme list) (t::typ). \
 \               free_tv (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
 \               free_tv A Un free_tv ($ S A) Un free_tv t Un free_tv ($ S t)";
-by (fast_tac (!claset addDs [dom_S' RS subsetD,cod_S' RS subsetD]) 1);
+by (fast_tac (claset() addDs [dom_S' RS subsetD,cod_S' RS subsetD]) 1);
 qed "free_tv_S'";
 
 goal thy "!!t1::typ. \
 \         (free_tv ($ (%x. TVar (if x : free_tv A then x else n + x)) t1) - free_tv A) <= \
 \         {x. ? y. x = n + y}";
 by (typ.induct_tac "t1" 1);
-by (simp_tac (!simpset addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsplits [expand_if]) 1);
 by (Fast_tac 1);
 by (Simp_tac 1);
 by (Fast_tac 1);
@@ -149,7 +149,7 @@
 by (list.induct_tac "A" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
-by (fast_tac (!claset addDs [new_tv_Int_free_tv_empty_scheme ]) 1);
+by (fast_tac (claset() addDs [new_tv_Int_free_tv_empty_scheme ]) 1);
 val new_tv_Int_free_tv_empty_scheme_list = result ();
 
 goalw thy [le_type_scheme_def,is_bound_typ_instance] 
@@ -167,7 +167,7 @@
 by (assume_tac 1);
 by (dtac new_tv_not_free_tv 1);
 by (dtac new_tv_not_free_tv 1);
-by (asm_simp_tac (!simpset addsimps [diff_add_inverse ]) 1);
+by (asm_simp_tac (simpset() addsimps [diff_add_inverse ]) 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed_spec_mp "gen_t_le_gen_alpha_t";
@@ -176,11 +176,11 @@
 
 goal thy "!!e. A |- e::t ==> !B. A <= B -->  B |- e::t";
 by (etac has_type.induct 1);
-   by (simp_tac (!simpset addsimps [le_env_def]) 1);
-   by (fast_tac (!claset addEs [bound_typ_instance_trans] addss !simpset) 1);
+   by (simp_tac (simpset() addsimps [le_env_def]) 1);
+   by (fast_tac (claset() addEs [bound_typ_instance_trans] addss simpset()) 1);
   by (Asm_full_simp_tac 1);
  by (Fast_tac 1);
-by (slow_tac (!claset addEs [le_env_free_tv RS free_tv_subset_gen_le]) 1);
+by (slow_tac (claset() addEs [le_env_free_tv RS free_tv_subset_gen_le]) 1);
 qed_spec_mp "has_type_le_env";
 
 (* has_type is closed w.r.t. substitution *)
@@ -189,8 +189,8 @@
 (* case VarI *)
    by (rtac allI 1);
    by (rtac has_type.VarI 1);
-    by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
-   by (asm_simp_tac (!simpset addsimps [app_subst_list]) 1);
+    by (asm_full_simp_tac (simpset() addsimps [app_subst_list]) 1);
+   by (asm_simp_tac (simpset() addsimps [app_subst_list]) 1);
   (* case AbsI *)
   by (rtac allI 1);
   by (Simp_tac 1);