1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Sun Jul 17 14:11:35 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Sun Jul 17 14:11:35 2011 +0200
     1.3 @@ -1369,8 +1369,7 @@
     1.4    level_of_type_enc type_enc <> No_Types andalso
     1.5    not (null (Term.hidden_polymorphism t))
     1.6  
     1.7 -fun helper_facts_for_sym ctxt format type_enc trans_lambdas
     1.8 -                         (s, {types, ...} : sym_info) =
     1.9 +fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
    1.10    case strip_prefix_and_unascii const_prefix s of
    1.11      SOME mangled_s =>
    1.12      let
    1.13 @@ -1392,7 +1391,7 @@
    1.14          end
    1.15          |> map (fn (k, t) => (dub needs_fairly_sound j k, t)) o tag_list 1
    1.16        val make_facts =
    1.17 -        map_filter (make_fact ctxt format type_enc trans_lambdas false false [])
    1.18 +        map_filter (make_fact ctxt format type_enc I false false [])
    1.19        val fairly_sound = is_type_enc_fairly_sound type_enc
    1.20      in
    1.21        helper_table
    1.22 @@ -1406,10 +1405,9 @@
    1.23                      |> make_facts)
    1.24      end
    1.25    | NONE => []
    1.26 -fun helper_facts_for_sym_table ctxt format type_enc trans_lambdas sym_tab =
    1.27 -  Symtab.fold_rev (append
    1.28 -                   o helper_facts_for_sym ctxt format type_enc trans_lambdas)
    1.29 -                  sym_tab []
    1.30 +fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
    1.31 +  Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
    1.32 +                  []
    1.33  
    1.34  (***************************************************************)
    1.35  (* Type Classes Present in the Axiom or Conjecture Clauses     *)
    1.36 @@ -1905,9 +1903,8 @@
    1.37      val repaired_sym_tab =
    1.38        conjs @ facts |> sym_table_for_facts ctxt (SOME false)
    1.39      val helpers =
    1.40 -      repaired_sym_tab
    1.41 -      |> helper_facts_for_sym_table ctxt format type_enc trans_lambdas
    1.42 -      |> map repair
    1.43 +      repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
    1.44 +                       |> map repair
    1.45      val poly_nonmono_Ts =
    1.46        if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
    1.47           polymorphism_of_type_enc type_enc <> Polymorphic then