1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Apr 23 10:23:26 2014 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Apr 23 10:23:26 2014 +0200
     1.3 @@ -1286,8 +1286,7 @@
     1.4  fun is_format_with_defs (THF _) = true
     1.5    | is_format_with_defs _ = false
     1.6  
     1.7 -fun make_fact ctxt format type_enc iff_for_eq
     1.8 -              ((name, stature as (_, status)), t) =
     1.9 +fun make_fact ctxt format type_enc iff_for_eq ((name, stature as (_, status)), t) =
    1.10    let
    1.11      val role =
    1.12        if is_format_with_defs format andalso status = Non_Rec_Def andalso
    1.13 @@ -1742,8 +1741,7 @@
    1.14  fun should_specialize_helper type_enc t =
    1.15    could_specialize_helpers type_enc andalso not (null (Term.hidden_polymorphism t))
    1.16  
    1.17 -fun add_helper_facts_of_sym ctxt format type_enc completish
    1.18 -                            (s, {types, ...} : sym_info) =
    1.19 +fun add_helper_facts_of_sym ctxt format type_enc completish (s, {types, ...} : sym_info) =
    1.20    (case unprefix_and_unascii const_prefix s of
    1.21      SOME mangled_s =>
    1.22      let
    1.23 @@ -1785,8 +1783,7 @@
    1.24      end
    1.25    | NONE => I)
    1.26  fun helper_facts_of_sym_table ctxt format type_enc completish sym_tab =
    1.27 -  Symtab.fold_rev (add_helper_facts_of_sym ctxt format type_enc completish)
    1.28 -                  sym_tab []
    1.29 +  Symtab.fold_rev (add_helper_facts_of_sym ctxt format type_enc completish) sym_tab []
    1.30  
    1.31  (***************************************************************)
    1.32  (* Type Classes Present in the Axiom or Conjecture Clauses     *)
    1.33 @@ -2438,24 +2435,31 @@
    1.34      val decl_lines = maps (lines_of_sym_decls ctxt mono type_enc) syms
    1.35    in mono_lines @ decl_lines end
    1.36  
    1.37 -fun datatypes_of_sym_table ctxt ctrss (DFG Polymorphic) (type_enc as Native _)
    1.38 -                           uncurried_aliases sym_tab =
    1.39 +fun datatypes_of_sym_table ctxt ctrss (DFG Polymorphic) (type_enc as Native _) uncurried_aliases
    1.40 +      sym_tab =
    1.41      if is_type_enc_polymorphic type_enc then
    1.42        let
    1.43          val thy = Proof_Context.theory_of ctxt
    1.44 +
    1.45          fun do_ctr (s, T) =
    1.46            let
    1.47              val s' = make_fixed_const (SOME type_enc) s
    1.48              val ary = ary_of T
    1.49 -            fun mk name = mk_aterm type_enc name (robust_const_type_args thy (s, T)) []
    1.50 +            fun mk name = SOME (mk_aterm type_enc name (robust_const_type_args thy (s, T)) [])
    1.51            in
    1.52 -            (case Symtab.lookup sym_tab s' of
    1.53 -              NONE => NONE
    1.54 -            | SOME ({min_ary, ...} : sym_info) =>
    1.55 -              if ary = min_ary then SOME (mk (s', s))
    1.56 -              else if uncurried_aliases then SOME (mk (aliased_uncurried ary (s', s)))
    1.57 -              else NONE)
    1.58 +            if T = HOLogic.boolT then
    1.59 +              (case proxify_const s' of
    1.60 +                SOME proxy_base => mk (proxy_base |>> prefix const_prefix)
    1.61 +              | NONE => NONE)
    1.62 +            else
    1.63 +              (case Symtab.lookup sym_tab s' of
    1.64 +                NONE => NONE
    1.65 +              | SOME ({min_ary, ...} : sym_info) =>
    1.66 +                if ary = min_ary then mk (s', s)
    1.67 +                else if uncurried_aliases then mk (aliased_uncurried ary (s', s))
    1.68 +                else NONE)
    1.69            end
    1.70 +
    1.71          fun datatype_of_ctrs (ctrs as (_, T1) :: _) =
    1.72            let val ctrs' = map do_ctr ctrs in
    1.73              if forall is_some ctrs' then
    1.74 @@ -2610,8 +2614,7 @@
    1.75                      | (s, (sym, ty)) => cons (Sym_Decl (sym_decl_prefix ^ s, sym, ty ()))) syms []
    1.76    in (heading, decls) :: problem end
    1.77  
    1.78 -fun all_ctrss_of_datatypes ctxt =
    1.79 -  map (map_filter (try dest_Const) o #ctrs) (Ctr_Sugar.ctr_sugars_of ctxt)
    1.80 +val all_ctrss_of_datatypes = map (map_filter (try dest_Const) o #ctrs) o Ctr_Sugar.ctr_sugars_of
    1.81  
    1.82  val app_op_and_predicator_threshold = 45
    1.83