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