--- a/src/Provers/clasimp.ML Sun Mar 01 16:48:06 2009 +0100
+++ b/src/Provers/clasimp.ML Sun Mar 01 23:36:12 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Provers/clasimp.ML
- ID: $Id$
Author: David von Oheimb, TU Muenchen
Combination of classical reasoner and simplifier (depends on
@@ -153,7 +152,7 @@
end;
fun modifier att (x, ths) =
- fst (foldl_map (Library.apply [att]) (x, rev ths));
+ fst (Library.foldl_map (Library.apply [att]) (x, rev ths));
val addXIs = modifier (ContextRules.intro_query NONE);
val addXEs = modifier (ContextRules.elim_query NONE);