# 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     *)