# HG changeset patch
# User wenzelm
# Date 969400946 -7200
# Node ID ca83cc2973f9bc7fc1c318c38bef2b66281702b1
# Parent  c095955e7575879c16f9016e3635c34e79de21b1
made SML/NJ happy;

diff -r c095955e7575 -r ca83cc2973f9 src/Provers/clasimp.ML
--- 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);