src/HOL/MiniML/Generalize.ML

 
 goal thy "!!A. bound_tv (gen A t1) = (free_tv t1) - (free_tv A)";
 by (typ.induct_tac "t1" 1);
 by (Simp_tac 1);
 by (case_tac "nat : free_tv A" 1);
-by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
-by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
 by (Fast_tac 1);
 by (Asm_simp_tac 1);
 by (Fast_tac 1);
 qed "bound_tv_gen";
 

 by (Asm_full_simp_tac 1);
 qed_spec_mp "new_tv_compatible_gen";
 
 goalw thy [gen_ML_def] "!!A. gen A t = gen_ML A t";
 by (typ.induct_tac "t" 1);
-by (simp_tac (!simpset addsimps [free_tv_ML_scheme_list]) 1);
-by (asm_simp_tac (!simpset addsimps [free_tv_ML_scheme_list]) 1);
+by (simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1);
+by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1);
 qed "gen_eq_gen_ML";
 
 goal thy "!!S. (free_tv S) Int ((free_tv t) - (free_tv A)) = {} \
 \          --> gen ($ S A) ($ S t) = $ S (gen A t)";
 by (typ.induct_tac "t" 1);

 by (case_tac "nat:(free_tv A)" 1);
 by (Asm_simp_tac 1);
 by (Asm_full_simp_tac 1);
 by (subgoal_tac "nat ~: free_tv S" 1);
 by (Fast_tac 2);
-by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,de_Morgan_disj]) 1);
+by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def,de_Morgan_disj]) 1);
 by (split_tac [expand_if] 1);
 by (cut_facts_tac [free_tv_app_subst_scheme_list] 1);
 by (Fast_tac 1);
 by (Asm_simp_tac 1);
 by (Best_tac 1);

 qed_spec_mp "bound_typ_inst_gen";
 Addsimps [bound_typ_inst_gen];
 
 goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance]
   "gen ($ S A) ($ S t) <= $ S (gen A t)";
-by (safe_tac (!claset));
+by (safe_tac (claset()));
 by (rename_tac "R" 1);
 by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
 by (typ.induct_tac "t" 1);
- by (simp_tac (!simpset addsplits [expand_if]) 1);
+ by (simp_tac (simpset() addsplits [expand_if]) 1);
 by (Asm_simp_tac 1);
 qed "gen_bound_typ_instance";
 
 goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance]
   "!!A B. free_tv B <= free_tv A ==> gen A t <= gen B t";
-by (safe_tac (!claset));
+by (safe_tac (claset()));
 by (rename_tac "S" 1);
 by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
 by (typ.induct_tac "t" 1);
- by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
+ by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
  by (Fast_tac 1);
 by (Asm_simp_tac 1);
 qed "free_tv_subset_gen_le";
 
 goalw thy [le_type_scheme_def,is_bound_typ_instance] 

 by (hyp_subst_tac 1);
 by (res_inst_tac [("x","(%x. S (if n <= x then x - n else x))")] exI 1);
 by (typ.induct_tac "t" 1);
 by (Simp_tac 1);
 by (case_tac "nat : free_tv A" 1);
-by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
-by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
 by (subgoal_tac "n <= n + nat" 1);
 by (forw_inst_tac [("t","A")] new_tv_le 1);
 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 (simp_tac (!simpset addsimps [le_add1]) 1);
+by (asm_simp_tac (simpset() addsimps [diff_add_inverse]) 1);
+by (simp_tac (simpset() addsimps [le_add1]) 1);
 by (Asm_simp_tac 1);
 qed_spec_mp "gen_t_le_gen_alpha_t";
 
 Addsimps [gen_t_le_gen_alpha_t];