backout 9579464d00f9 to avoid odd crash of polyml-5.2.1 (according to Jasmin, this change is not essential for now);
1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed May 02 22:40:28 2012 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu May 03 13:17:15 2012 +0200
1.3 @@ -1681,7 +1681,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 add_helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
1.8 +fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
1.9 case unprefix_and_unascii const_prefix s of
1.10 SOME mangled_s =>
1.11 let
1.12 @@ -1705,20 +1705,20 @@
1.13 val make_facts = map_filter (make_fact ctxt format type_enc false)
1.14 val fairly_sound = is_type_enc_fairly_sound type_enc
1.15 in
1.16 - fold (fn ((helper_s, needs_fairly_sound), ths) =>
1.17 - if helper_s <> unmangled_s orelse
1.18 - (needs_fairly_sound andalso not fairly_sound) then
1.19 - I
1.20 - else
1.21 - ths ~~ (1 upto length ths)
1.22 - |> maps (dub_and_inst needs_fairly_sound)
1.23 - |> make_facts
1.24 - |> union (op = o pairself #iformula))
1.25 - helper_table
1.26 + helper_table
1.27 + |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
1.28 + if helper_s <> unmangled_s orelse
1.29 + (needs_fairly_sound andalso not fairly_sound) then
1.30 + []
1.31 + else
1.32 + ths ~~ (1 upto length ths)
1.33 + |> maps (dub_and_inst needs_fairly_sound)
1.34 + |> make_facts)
1.35 end
1.36 - | NONE => I
1.37 + | NONE => []
1.38 fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
1.39 - Symtab.fold_rev (add_helper_facts_for_sym ctxt format type_enc) sym_tab []
1.40 + Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
1.41 + []
1.42
1.43 (***************************************************************)
1.44 (* Type Classes Present in the Axiom or Conjecture Clauses *)