# HG changeset patch
# User blanchet
# Date 1321702941 -3600
# Node ID dc9a7ff13e37ba4b3e76b23a23b9c221cccf3187
# Parent  78f59aaa30ffd2b15635f07c4cd439a4522b6c73
made SML/NJ happy

diff -r 78f59aaa30ff -r dc9a7ff13e37 src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Fri Nov 18 22:32:57 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Sat Nov 19 12:42:21 2011 +0100
@@ -48,7 +48,7 @@
     Proof.context -> (string * locality) list vector -> string proof
     -> (string * locality) list
   val lam_trans_from_atp_proof : string proof -> string -> string
-  val is_typed_helper_used_in_proof : string proof -> bool
+  val is_typed_helper_used_in_atp_proof : string proof -> bool
   val used_facts_in_unsound_atp_proof :
     Proof.context -> (string * locality) list vector -> 'a proof
     -> string list option
@@ -175,7 +175,8 @@
 
 val is_typed_helper_name =
   String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
-val is_typed_helper_used_in_proof = is_axiom_used_in_proof is_typed_helper_name
+fun is_typed_helper_used_in_atp_proof atp_proof =
+  is_axiom_used_in_proof is_typed_helper_name atp_proof
 
 val leo2_ext = "extcnf_equal_neg"
 val isa_ext = Thm.get_name_hint @{thm ext}
@@ -1026,7 +1027,7 @@
     val frees = fold Term.add_frees (concl_t :: hyp_ts) []
     val one_line_proof = one_line_proof_text one_line_params
     val type_enc =
-      if is_typed_helper_used_in_proof atp_proof then full_typesN
+      if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
       else partial_typesN
     val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans
     fun isar_proof_for () =
diff -r 78f59aaa30ff -r dc9a7ff13e37 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Nov 18 22:32:57 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Nov 19 12:42:21 2011 +0100
@@ -790,7 +790,7 @@
         NONE =>
         let
           val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
-          val needs_full_types = is_typed_helper_used_in_proof atp_proof
+          val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
           val reconstrs =
             bunch_of_reconstructors needs_full_types
                 (lam_trans_from_atp_proof atp_proof