diff -r 9f1eaab75e8c -r 771b1f6422a8 src/ZF/ex/Mutil.ML
--- a/src/ZF/ex/Mutil.ML	Mon Nov 03 12:22:43 1997 +0100
+++ b/src/ZF/ex/Mutil.ML	Mon Nov 03 12:24:13 1997 +0100
@@ -23,22 +23,22 @@
 bind_thm("Finite_evnodd", evnodd_subset RS subset_imp_lepoll RS lepoll_Finite);
 
 goalw thy [evnodd_def] "evnodd(A Un B, b) = evnodd(A,b) Un evnodd(B,b)";
-by (simp_tac (!simpset addsimps [Collect_Un]) 1);
+by (simp_tac (simpset() addsimps [Collect_Un]) 1);
 qed "evnodd_Un";
 
 goalw thy [evnodd_def] "evnodd(A - B, b) = evnodd(A,b) - evnodd(B,b)";
-by (simp_tac (!simpset addsimps [Collect_Diff]) 1);
+by (simp_tac (simpset() addsimps [Collect_Diff]) 1);
 qed "evnodd_Diff";
 
 goalw thy [evnodd_def]
     "evnodd(cons(<i,j>,C), b) = \
 \    if((i#+j) mod 2 = b, cons(<i,j>, evnodd(C,b)), evnodd(C,b))";
-by (asm_simp_tac (!simpset addsimps [evnodd_def, Collect_cons] 
+by (asm_simp_tac (simpset() addsimps [evnodd_def, Collect_cons] 
                         setloop split_tac [expand_if]) 1);
 qed "evnodd_cons";
 
 goalw thy [evnodd_def] "evnodd(0, b) = 0";
-by (simp_tac (!simpset addsimps [evnodd_def]) 1);
+by (simp_tac (simpset() addsimps [evnodd_def]) 1);
 qed "evnodd_0";
 
 Addsimps [evnodd_cons, evnodd_0];
@@ -46,7 +46,7 @@
 (*** Dominoes ***)
 
 goal thy "!!d. d:domino ==> Finite(d)";
-by (blast_tac (!claset addSIs [Finite_cons, Finite_0] addEs [domino.elim]) 1);
+by (blast_tac (claset() addSIs [Finite_cons, Finite_0] addEs [domino.elim]) 1);
 qed "domino_Finite";
 
 goal thy "!!d. [| d:domino; b<2 |] ==> EX i' j'. evnodd(d,b) = {<i',j'>}";
@@ -55,9 +55,9 @@
 by (res_inst_tac [("k1", "i#+j")] (mod2_cases RS disjE) 1);
 by (REPEAT_FIRST (ares_tac [add_type]));
 (*Four similar cases: case (i#+j) mod 2 = b, 2#-b, ...*)
-by (REPEAT (asm_simp_tac (!simpset addsimps [mod_succ, succ_neq_self] 
+by (REPEAT (asm_simp_tac (simpset() addsimps [mod_succ, succ_neq_self] 
                                    setloop split_tac [expand_if]) 1
-           THEN blast_tac (!claset addDs [ltD]) 1));
+           THEN blast_tac (claset() addDs [ltD]) 1));
 qed "domino_singleton";
 
 
@@ -68,51 +68,51 @@
 goal thy "!!t. t: tiling(A) ==> \
 \              u: tiling(A) --> t Int u = 0 --> t Un u : tiling(A)";
 by (etac tiling.induct 1);
-by (simp_tac (!simpset addsimps tiling.intrs) 1);
-by (asm_full_simp_tac (!simpset addsimps [Un_assoc,
+by (simp_tac (simpset() addsimps tiling.intrs) 1);
+by (asm_full_simp_tac (simpset() addsimps [Un_assoc,
 					  subset_empty_iff RS iff_sym]) 1);
-by (blast_tac (!claset addIs tiling.intrs) 1);
+by (blast_tac (claset() addIs tiling.intrs) 1);
 qed_spec_mp "tiling_UnI";
 
 goal thy "!!t. t:tiling(domino) ==> Finite(t)";
 by (eresolve_tac [tiling.induct] 1);
 by (resolve_tac [Finite_0] 1);
-by (blast_tac (!claset addSIs [Finite_Un] addIs [domino_Finite]) 1);
+by (blast_tac (claset() addSIs [Finite_Un] addIs [domino_Finite]) 1);
 qed "tiling_domino_Finite";
 
 goal thy "!!t. t: tiling(domino) ==> |evnodd(t,0)| = |evnodd(t,1)|";
 by (eresolve_tac [tiling.induct] 1);
-by (simp_tac (!simpset addsimps [evnodd_def]) 1);
+by (simp_tac (simpset() addsimps [evnodd_def]) 1);
 by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1);
 by (Simp_tac 2 THEN assume_tac 1);
 by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1);
 by (Simp_tac 2 THEN assume_tac 1);
 by (Step_tac 1);
 by (subgoal_tac "ALL p b. p:evnodd(a,b) --> p~:evnodd(ta,b)" 1);
-by (asm_simp_tac (!simpset addsimps [evnodd_Un, Un_cons, tiling_domino_Finite,
+by (asm_simp_tac (simpset() addsimps [evnodd_Un, Un_cons, tiling_domino_Finite,
                                   evnodd_subset RS subset_Finite,
                                   Finite_imp_cardinal_cons]) 1);
-by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
+by (blast_tac (claset() addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
 qed "tiling_domino_0_1";
 
 goal thy "!!i n. [| i: nat;  n: nat |] ==> {i} * (n #+ n) : tiling(domino)";
 by (nat_ind_tac "n" [] 1);
-by (simp_tac (!simpset addsimps tiling.intrs) 1);
-by (asm_simp_tac (!simpset addsimps [Un_assoc RS sym, Sigma_succ2]) 1);
+by (simp_tac (simpset() addsimps tiling.intrs) 1);
+by (asm_simp_tac (simpset() addsimps [Un_assoc RS sym, Sigma_succ2]) 1);
 by (resolve_tac tiling.intrs 1);
 by (assume_tac 2);
 by (subgoal_tac    (*seems the easiest way of turning one to the other*)
     "{i}*{succ(n1#+n1)} Un {i}*{n1#+n1} = {<i,n1#+n1>, <i,succ(n1#+n1)>}" 1);
 by (Blast_tac 2);
-by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
-by (blast_tac (!claset addEs [mem_irrefl, mem_asym]) 1);
+by (asm_simp_tac (simpset() addsimps [domino.horiz]) 1);
+by (blast_tac (claset() addEs [mem_irrefl, mem_asym]) 1);
 qed "dominoes_tile_row";
 
 goal thy "!!m n. [| m: nat;  n: nat |] ==> m * (n #+ n) : tiling(domino)";
 by (nat_ind_tac "m" [] 1);
-by (simp_tac (!simpset addsimps tiling.intrs) 1);
-by (asm_simp_tac (!simpset addsimps [Sigma_succ1]) 1);
-by (blast_tac (!claset addIs [tiling_UnI, dominoes_tile_row] 
+by (simp_tac (simpset() addsimps tiling.intrs) 1);
+by (asm_simp_tac (simpset() addsimps [Sigma_succ1]) 1);
+by (blast_tac (claset() addIs [tiling_UnI, dominoes_tile_row] 
                     addEs [mem_irrefl]) 1);
 qed "dominoes_tile_matrix";
 
@@ -124,23 +124,23 @@
 by (resolve_tac [notI] 1);
 by (dresolve_tac [tiling_domino_0_1] 1);
 by (subgoal_tac "|evnodd(t',0)| < |evnodd(t',1)|" 1);
-by (asm_full_simp_tac (!simpset addsimps [lt_not_refl]) 1);
+by (asm_full_simp_tac (simpset() addsimps [lt_not_refl]) 1);
 by (subgoal_tac "t : tiling(domino)" 1);
 (*Requires a small simpset that won't move the succ applications*)
 by (asm_simp_tac (ZF_ss addsimps [nat_succI, add_type, 
                                   dominoes_tile_matrix]) 2);
 by (subgoal_tac "(m#+m)#+(n#+n) = (m#+n)#+(m#+n)" 1);
-by (asm_simp_tac (!simpset addsimps add_ac) 2);
+by (asm_simp_tac (simpset() addsimps add_ac) 2);
 by (asm_full_simp_tac 
-    (!simpset addsimps [evnodd_Diff, mod2_add_self,
+    (simpset() addsimps [evnodd_Diff, mod2_add_self,
                         mod2_succ_succ, tiling_domino_0_1 RS sym]) 1);
 by (resolve_tac [lt_trans] 1);
 by (REPEAT
     (rtac Finite_imp_cardinal_Diff 1 
      THEN
-     asm_simp_tac (!simpset addsimps [tiling_domino_Finite, Finite_evnodd, 
+     asm_simp_tac (simpset() addsimps [tiling_domino_Finite, Finite_evnodd, 
                                       Finite_Diff]) 1 
      THEN
-     asm_simp_tac (!simpset addsimps [evnodd_iff, nat_0_le RS ltD, 
+     asm_simp_tac (simpset() addsimps [evnodd_iff, nat_0_le RS ltD, 
                                       mod2_add_self]) 1));
 qed "mutil_not_tiling";