1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Jan 18 00:18:11 2013 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Jan 18 14:33:16 2013 +0100
     1.3 @@ -849,7 +849,7 @@
     1.4  
     1.5  fun filter_type_args thy constrs type_enc s ary T_args =
     1.6    let val poly = polymorphism_of_type_enc type_enc in
     1.7 -    if s = type_tag_name then (* ### FIXME: why not "type_guard_name" as well? *)
     1.8 +    if s = type_tag_name then (* FIXME: why not "type_guard_name" as well? *)
     1.9        T_args
    1.10      else case type_enc of
    1.11        Native (_, Raw_Polymorphic _, _) => T_args
    1.12 @@ -1580,7 +1580,7 @@
    1.13      fun add_iterm_syms conj_fact =
    1.14        add_iterm_syms_to_sym_table ctxt app_op_level conj_fact true
    1.15      fun add_fact_syms conj_fact =
    1.16 -      K (add_iterm_syms conj_fact) |> formula_fold NONE |> ifact_lift
    1.17 +      ifact_lift (formula_fold NONE (K (add_iterm_syms conj_fact)))
    1.18    in
    1.19      ((false, []), Symtab.empty)
    1.20      |> fold (add_fact_syms true) conjs
    1.21 @@ -2243,7 +2243,7 @@
    1.22           | _ => I)
    1.23          #> fold add_iterm_syms args
    1.24        end
    1.25 -    val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> ifact_lift
    1.26 +    val add_fact_syms = ifact_lift (formula_fold NONE (K add_iterm_syms))
    1.27      fun add_formula_var_types (ATyQuant (_, _, phi)) = add_formula_var_types phi
    1.28        | add_formula_var_types (AQuant (_, xs, phi)) =
    1.29          fold (fn (_, SOME T) => insert_type thy I T | _ => I) xs
    1.30 @@ -2291,8 +2291,8 @@
    1.31       | _ => known_infinite_types,
    1.32     maybe_nonmono_Ts = [if completish then tvar_a else @{typ bool}]}
    1.33  
    1.34 -(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
    1.35 -   out with monotonicity" paper presented at CADE 2011. *)
    1.36 +(* This inference is described in section 4 of Blanchette et al., "Encoding
    1.37 +   monomorphic and polymorphic types", TACAS 2013. *)
    1.38  fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono
    1.39    | add_iterm_mononotonicity_info ctxt level _
    1.40          (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
    1.41 @@ -2338,8 +2338,10 @@
    1.42        | add_args _ = I
    1.43      and add_term tm = add_type (ityp_of tm) #> add_args tm
    1.44    in formula_fold NONE (K add_term) end
    1.45 +
    1.46  fun add_fact_monotonic_types ctxt mono type_enc =
    1.47 -  add_iformula_monotonic_types ctxt mono type_enc |> ifact_lift
    1.48 +  ifact_lift (add_iformula_monotonic_types ctxt mono type_enc)
    1.49 +
    1.50  fun monotonic_types_for_facts ctxt mono type_enc facts =
    1.51    let val level = level_of_type_enc type_enc in
    1.52      [] |> (is_type_enc_polymorphic type_enc andalso
    1.53 @@ -2396,8 +2398,7 @@
    1.54                     ? curry APi (map (tvar_name o dest_TVar) T_args))
    1.55    end
    1.56  
    1.57 -fun honor_conj_sym_role in_conj =
    1.58 -  if in_conj then (Hypothesis, I) else (Axiom, I)
    1.59 +fun honor_conj_sym_role in_conj = (if in_conj then Hypothesis else Axiom, I)
    1.60  
    1.61  fun line_for_guards_sym_decl ctxt mono type_enc n s j
    1.62                               (s', T_args, T, _, ary, in_conj) =

     2.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Fri Jan 18 00:18:11 2013 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Fri Jan 18 14:33:16 2013 +0100
     2.3 @@ -156,12 +156,11 @@
     2.4      let
     2.5        val tvars = Term.add_tvar_namesT T []
     2.6        val tvars' = Term.add_tvar_namesT T' []
     2.7 +      val maxidx' = maxidx_of_typ T'
     2.8        val T =
     2.9 -        if exists (member (op =) tvars') tvars then
    2.10 -          T |> Logic.incr_tvar (maxidx_of_typ T' + 1)
    2.11 -        else
    2.12 -          T
    2.13 -    in can (Sign.typ_unify thy (T, T')) (Vartab.empty, 0) end
    2.14 +        T |> exists (member (op =) tvars') tvars ? Logic.incr_tvar (maxidx' + 1)
    2.15 +      val maxidx = Integer.max (maxidx_of_typ T) maxidx'
    2.16 +    in can (Sign.typ_unify thy (T, T')) (Vartab.empty, maxidx) end
    2.17  
    2.18  val type_equiv = Sign.typ_equiv
    2.19