# HG changeset patch
# User blanchet
# Date 1280232755 -7200
# Node ID cd67805a36b902e4f6d1874064567f32f88af9f0
# Parent  ae3df22dd70b93b0da725c0f24cffa679adca12a
no polymorphic "var"

diff -r ae3df22dd70b -r cd67805a36b9 src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Tue Jul 27 14:02:15 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Tue Jul 27 14:12:35 2010 +0200
@@ -387,7 +387,8 @@
 fun repair_problem_line thy explicit_forall full_types const_tab
                         (Fof (ident, kind, phi)) =
   Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
-val repair_problem_with_const_table = map o apsnd o map oooo repair_problem_line
+fun repair_problem_with_const_table thy =
+  map o apsnd o map ooo repair_problem_line thy
 
 fun repair_problem thy explicit_forall full_types explicit_apply problem =
   repair_problem_with_const_table thy explicit_forall full_types