# HG changeset patch
# User blanchet
# Date 1279790971 -7200
# Node ID 7b452ff6bff074f5ca85f1ac217d94c7ff24215d
# Parent  38e71ffc8fe8dc8bdcd62e4f30e39dd4098c3b4a
no polymorphic "var"s

diff -r 38e71ffc8fe8 -r 7b452ff6bff0 src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Thu Jul 22 08:37:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Thu Jul 22 11:29:31 2010 +0200
@@ -102,9 +102,9 @@
 fun nice_atp_literal (pos, t) = nice_atp_term t #>> pair pos
 fun nice_problem_line (Cnf (ident, kind, lits)) =
   pool_map nice_atp_literal lits #>> (fn lits => Cnf (ident, kind, lits))
-val nice_problem =
+fun nice_problem problem =
   pool_map (fn (heading, lines) =>
-               pool_map nice_problem_line lines #>> pair heading)
+               pool_map nice_problem_line lines #>> pair heading) problem
 
 
 (** Sledgehammer stuff **)
@@ -214,7 +214,7 @@
   #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
 fun consider_literal (_, t) = consider_term true t
 fun consider_problem_line (Cnf (_, _, lits)) = fold consider_literal lits
-val consider_problem = fold (fold consider_problem_line o snd)
+fun consider_problem problem = fold (fold consider_problem_line o snd) problem
 
 fun const_table_for_problem explicit_apply problem =
   if explicit_apply then NONE
@@ -293,8 +293,8 @@
           |> repair_predicates_in_term const_tab)
 fun repair_problem_line thy full_types const_tab (Cnf (ident, kind, lits)) =
   Cnf (ident, kind, map (repair_literal thy full_types const_tab) lits)
-val repair_problem_with_const_table = map o apsnd o map ooo repair_problem_line
-
+fun repair_problem_with_const_table thy full_types const_tab problem =
+  map (apsnd (map (repair_problem_line thy full_types const_tab))) problem
 fun repair_problem thy full_types explicit_apply problem =
   repair_problem_with_const_table thy full_types
       (const_table_for_problem explicit_apply problem) problem