src/ZF/Resid/Confluence.ML

--- a/src/ZF/Resid/Confluence.ML	Mon Nov 03 12:22:43 1997 +0100
+++ b/src/ZF/Resid/Confluence.ML	Mon Nov 03 12:24:13 1997 +0100
@@ -16,7 +16,7 @@
 by (resolve_tac [impI RS allI RS allI] 1);
 by (etac Spar_red.induct 1);
 by (Fast_tac  1);
-by (fast_tac (!claset addIs [Spar_red.trans]) 1);
+by (fast_tac (claset() addIs [Spar_red.trans]) 1);
 qed "strip_lemma_r";
 
 
@@ -29,7 +29,7 @@
 by (dres_inst_tac [("x1","z")] (spec RS mp) 1);
 by (REPEAT(eresolve_tac [exE,conjE] 2));
 by (dres_inst_tac [("x1","ua")] (spec RS mp) 2);
-by (fast_tac (!claset addIs [Spar_red.trans]) 3);
+by (fast_tac (claset() addIs [Spar_red.trans]) 3);
 by (TRYALL assume_tac );
 qed "strip_lemma_l";
 
@@ -45,7 +45,7 @@
 by (Clarify_tac 1);
 by (forw_inst_tac [("v","va")] paving 1);
 by (TRYALL assume_tac);
-by (fast_tac (!claset addIs [completeness] addss (!simpset)) 1);
+by (fast_tac (claset() addIs [completeness] addss (simpset())) 1);
 qed "parallel_moves";
 
 bind_thm ("confluence_parallel_reduction",
@@ -53,7 +53,7 @@
 
 goalw Confluence.thy [confluence_def] 
     "!!u.[|confluence(Spar_red)|]==> confluence(Sred)";
-by(blast_tac (!claset addIs [par_red_red, red_par_red]) 1);
+by(blast_tac (claset() addIs [par_red_red, red_par_red]) 1);
 val lemma1 = result();
 
 bind_thm ("confluence_beta_reduction",