--- a/src/HOL/Induct/Comb.ML Thu May 15 15:51:09 1997 +0200
+++ b/src/HOL/Induct/Comb.ML Thu May 15 15:51:47 1997 +0200
@@ -54,7 +54,6 @@
AddSIs [contract.K, contract.S];
AddIs [contract.Ap1, contract.Ap2];
AddSEs [K_contractE, S_contractE, Ap_contractE];
-Unsafe_Addss (!simpset);
goalw Comb.thy [I_def] "!!z. I -1-> z ==> P";
by (Blast_tac 1);
@@ -105,7 +104,6 @@
AddIs parcontract.intrs;
AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE];
-Unsafe_Addss (!simpset);
(*** Basic properties of parallel contraction ***)