src/ZF/QUniv.ML

--- a/src/ZF/QUniv.ML	Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/QUniv.ML	Fri Sep 17 16:16:38 1993 +0200
@@ -205,7 +205,7 @@
 
 goalw QUniv.thy [QPair_def,sum_def]
     "<a;b> Int quniv(A) = <a;b> Int univ(eclose(A))";
-by (SIMP_TAC (ZF_ss addrews [Int_Un_distrib, product_Int_quniv_eq]) 1);
+by (simp_tac (ZF_ss addsimps [Int_Un_distrib, product_Int_quniv_eq]) 1);
 val QPair_Int_quniv_eq = result();
 
 (**** "Take-lemma" rules for proving c: quniv(A) ****)