--- a/src/Provers/clasimp.ML Tue Sep 19 23:54:25 2000 +0200
+++ b/src/Provers/clasimp.ML Wed Sep 20 00:02:26 2000 +0200
@@ -155,7 +155,8 @@
val op addIffs =
foldl (addIff Classical.addSDs Classical.addSEs Classical.addSIs Simplifier.addsimps);
val addIffs' =
- foldl (addIff Classical.addXDs Classical.addXEs Classical.addXIs (fn (ss, _) => ss));
+ foldl (addIff Classical.addXDs Classical.addXEs Classical.addXIs
+ ((fn (ss, _) => ss): Simplifier.simpset * thm list -> Simplifier.simpset));
val op delIffs = foldl delIff;
fun AddIffs thms = store_clasimp ((Classical.claset (), Simplifier.simpset ()) addIffs thms);