avoid duplicate helpers
authorblanchet
Fri Apr 27 22:36:27 2012 +0200 (2012-04-27)
changeset 478109579464d00f9
parent 47809 4d8cbea248b0
child 47811 1e8eb643540d
avoid duplicate helpers
src/HOL/Tools/ATP/atp_problem_generate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Apr 27 21:24:30 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Apr 27 22:36:27 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 helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
     1.8 +fun add_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 -      helper_table
    1.17 -      |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
    1.18 -                  if helper_s <> unmangled_s orelse
    1.19 -                     (needs_fairly_sound andalso not fairly_sound) then
    1.20 -                    []
    1.21 -                  else
    1.22 -                    ths ~~ (1 upto length ths)
    1.23 -                    |> maps (dub_and_inst needs_fairly_sound)
    1.24 -                    |> make_facts)
    1.25 +      fold (fn ((helper_s, needs_fairly_sound), ths) =>
    1.26 +               if helper_s <> unmangled_s orelse
    1.27 +                  (needs_fairly_sound andalso not fairly_sound) then
    1.28 +                 I
    1.29 +               else
    1.30 +                 ths ~~ (1 upto length ths)
    1.31 +                 |> maps (dub_and_inst needs_fairly_sound)
    1.32 +                 |> make_facts
    1.33 +                 |> union (op = o pairself #iformula))
    1.34 +           helper_table
    1.35      end
    1.36 -  | NONE => []
    1.37 +  | NONE => I
    1.38  fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
    1.39 -  Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
    1.40 -                  []
    1.41 +  Symtab.fold_rev (add_helper_facts_for_sym ctxt format type_enc) sym_tab []
    1.42  
    1.43  (***************************************************************)
    1.44  (* Type Classes Present in the Axiom or Conjecture Clauses     *)