--- a/src/ZF/ex/misc.ML Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/ex/misc.ML Wed Nov 05 13:14:15 1997 +0100
@@ -45,7 +45,7 @@
\ (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) --> \
\ J : hom(A,f,B,g) & K : hom(B,g,C,h) --> \
\ (K O J) : hom(A,f,C,h)";
-by (asm_simp_tac (simpset() setloop (K (safe_tac (claset())))) 1);
+by (asm_simp_tac (simpset() setloop (K Safe_tac)) 1);
val comp_homs = result();
(*This version uses meta-level rewriting, safe_tac and asm_simp_tac*)
@@ -56,7 +56,7 @@
\ J : hom(A,f,B,g) & K : hom(B,g,C,h) --> \
\ (K O J) : hom(A,f,C,h)";
by (rewtac hom_def);
-by (safe_tac (claset()));
+by Safe_tac;
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
qed "comp_homs";