# HG changeset patch
# User krauss
# Date 1272742143 -7200
# Node ID e5f7235f39c5b4b38b8fadf552360eb21a78c728
# Parent  5479681ab465f5d6bcb8fbb22092cdb44bf44616
made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)

diff -r 5479681ab465 -r e5f7235f39c5 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat May 01 20:49:39 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat May 01 21:29:03 2010 +0200
@@ -130,7 +130,7 @@
   type T = raw_param list
   val empty = map (apsnd single) default_default_params
   val extend = I
-  val merge = AList.merge (op =) (K true))
+  fun merge (x, y) = AList.merge (op =) (K true) (x, y))
 
 val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param
 val default_raw_params = Data.get
diff -r 5479681ab465 -r e5f7235f39c5 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat May 01 20:49:39 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat May 01 21:29:03 2010 +0200
@@ -62,7 +62,7 @@
   type T = (typ * term_postprocessor) list
   val empty = []
   val extend = I
-  val merge = AList.merge (op =) (K true))
+  fun merge (x, y) = AList.merge (op =) (K true) (x, y))
 
 val irrelevant = "_"
 val unknown = "?"
diff -r 5479681ab465 -r e5f7235f39c5 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Sat May 01 20:49:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Sat May 01 21:29:03 2010 +0200
@@ -62,7 +62,8 @@
       filtered_clauses = SOME (the_default axclauses filtered_clauses)}
   in
     prover params (K "") timeout problem
-    |> tap (priority o string_for_outcome o #outcome)
+    |> tap (fn result : prover_result =>
+         priority (string_for_outcome (#outcome result)))
   end
 
 (* minimalization of thms *)
diff -r 5479681ab465 -r e5f7235f39c5 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat May 01 20:49:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat May 01 21:29:03 2010 +0200
@@ -35,7 +35,7 @@
 
 (** Attribute for converting a theorem into clauses **)
 
-val parse_clausify_attribute =
+val parse_clausify_attribute : attribute context_parser =
   Scan.lift OuterParse.nat
   >> (fn i => Thm.rule_attribute (fn context => fn th =>
                   let val thy = Context.theory_of context in
diff -r 5479681ab465 -r e5f7235f39c5 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Sat May 01 20:49:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Sat May 01 21:29:03 2010 +0200
@@ -48,7 +48,8 @@
   Long_Name.base_name
   #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
 
-val index_in_shape = find_index o exists o curry (op =)
+val index_in_shape : int -> int list list -> int =
+  find_index o exists o curry (op =)
 fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names
 fun is_conjecture_clause_number conjecture_shape num =
   index_in_shape num conjecture_shape >= 0