# HG changeset patch
# User blanchet
# Date 1310904695 -7200
# Node ID be41d12de6fa61d45cb7f85d814b5bc5ff981eb5
# Parent  a875729380a4dd26091e0b0d521f554f0b57e987
simplify code -- there are no lambdas in helpers anyway

diff -r a875729380a4 -r be41d12de6fa src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Sun Jul 17 14:11:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Sun Jul 17 14:11:35 2011 +0200
@@ -1369,8 +1369,7 @@
   level_of_type_enc type_enc <> No_Types andalso
   not (null (Term.hidden_polymorphism t))
 
-fun helper_facts_for_sym ctxt format type_enc trans_lambdas
-                         (s, {types, ...} : sym_info) =
+fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
   case strip_prefix_and_unascii const_prefix s of
     SOME mangled_s =>
     let
@@ -1392,7 +1391,7 @@
         end
         |> map (fn (k, t) => (dub needs_fairly_sound j k, t)) o tag_list 1
       val make_facts =
-        map_filter (make_fact ctxt format type_enc trans_lambdas false false [])
+        map_filter (make_fact ctxt format type_enc I false false [])
       val fairly_sound = is_type_enc_fairly_sound type_enc
     in
       helper_table
@@ -1406,10 +1405,9 @@
                     |> make_facts)
     end
   | NONE => []
-fun helper_facts_for_sym_table ctxt format type_enc trans_lambdas sym_tab =
-  Symtab.fold_rev (append
-                   o helper_facts_for_sym ctxt format type_enc trans_lambdas)
-                  sym_tab []
+fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
+  Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
+                  []
 
 (***************************************************************)
 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
@@ -1905,9 +1903,8 @@
     val repaired_sym_tab =
       conjs @ facts |> sym_table_for_facts ctxt (SOME false)
     val helpers =
-      repaired_sym_tab
-      |> helper_facts_for_sym_table ctxt format type_enc trans_lambdas
-      |> map repair
+      repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
+                       |> map repair
     val poly_nonmono_Ts =
       if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
          polymorphism_of_type_enc type_enc <> Polymorphic then