# HG changeset patch # User wenzelm # Date 1336043835 -7200 # Node ID 6ea205a4d7fd0627c434c3f92544570f46f9c61a # Parent 271980472765f74dd66373d0fbbfc19a5dc2f362 backout 9579464d00f9 to avoid odd crash of polyml-5.2.1 (according to Jasmin, this change is not essential for now); diff -r 271980472765 -r 6ea205a4d7fd src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed May 02 22:40:28 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu May 03 13:17:15 2012 +0200 @@ -1681,7 +1681,7 @@ level_of_type_enc type_enc <> No_Types andalso not (null (Term.hidden_polymorphism t)) -fun add_helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) = +fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) = case unprefix_and_unascii const_prefix s of SOME mangled_s => let @@ -1705,20 +1705,20 @@ val make_facts = map_filter (make_fact ctxt format type_enc false) val fairly_sound = is_type_enc_fairly_sound type_enc in - fold (fn ((helper_s, needs_fairly_sound), ths) => - if helper_s <> unmangled_s orelse - (needs_fairly_sound andalso not fairly_sound) then - I - else - ths ~~ (1 upto length ths) - |> maps (dub_and_inst needs_fairly_sound) - |> make_facts - |> union (op = o pairself #iformula)) - helper_table + helper_table + |> maps (fn ((helper_s, needs_fairly_sound), ths) => + if helper_s <> unmangled_s orelse + (needs_fairly_sound andalso not fairly_sound) then + [] + else + ths ~~ (1 upto length ths) + |> maps (dub_and_inst needs_fairly_sound) + |> make_facts) end - | NONE => I + | NONE => [] fun helper_facts_for_sym_table ctxt format type_enc sym_tab = - Symtab.fold_rev (add_helper_facts_for_sym 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 *)