src/ZF/Coind/Types.ML

--- a/src/ZF/Coind/Types.ML	Tue Sep 22 13:49:22 1998 +0200
+++ b/src/ZF/Coind/Types.ML	Tue Sep 22 13:50:57 1998 +0200
@@ -15,13 +15,13 @@
 
 Goal "te_rec(te_emp,c_te_emp,f_te_owr) = c_te_emp";
 by (rtac (te_rec_def RS def_Vrec RS trans) 1);
-by (simp_tac (simpset() addsimps (rank_te_owr1::TyEnv.case_eqns)) 1);
+by (simp_tac (simpset() addsimps rank_te_owr1::TyEnv.case_eqns) 1);
 qed "te_rec_emp";
 
 Goal " te_rec(te_owr(te,x,t),c_te_emp,f_te_owr) = \
 \   f_te_owr(te,x,t,te_rec(te,c_te_emp,f_te_owr))";
 by (rtac (te_rec_def RS def_Vrec RS trans) 1);
-by (simp_tac (rank_ss addsimps (rank_te_owr1::TyEnv.case_eqns)) 1);
+by (simp_tac (rank_ss addsimps rank_te_owr1::TyEnv.case_eqns) 1);
 qed "te_rec_owr";
 
 Goalw [te_dom_def] "te_dom(te_emp) = 0";