1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 16:20:18 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 16:20:18 2011 +0200
     1.3 @@ -1005,7 +1005,7 @@
     1.4                  t |> preproc ?
     1.5                       (preprocess_prop ctxt presimp_consts kind #> freeze_term)
     1.6                    |> make_formula thy format type_sys (format <> CNF)
     1.7 -                                  (string_of_int j) General kind
     1.8 +                                  (string_of_int j) Local kind
     1.9                    |> maybe_negate
    1.10                end)
    1.11           (0 upto last) ts
    1.12 @@ -1648,21 +1648,22 @@
    1.13  
    1.14  (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
    1.15     out with monotonicity" paper presented at CADE 2011. *)
    1.16 -fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I
    1.17 -  | add_combterm_nonmonotonic_types ctxt level _
    1.18 +fun add_combterm_nonmonotonic_types _ _ _ (SOME false) _ = I
    1.19 +  | add_combterm_nonmonotonic_types ctxt level locality _
    1.20          (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1),
    1.21                             tm2)) =
    1.22      (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
    1.23       (case level of
    1.24          Nonmonotonic_Types =>
    1.25 +        not (is_locality_global locality) orelse
    1.26          not (is_type_surely_infinite ctxt known_infinite_types T)
    1.27        | Finite_Types => is_type_surely_finite ctxt T
    1.28        | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
    1.29 -  | add_combterm_nonmonotonic_types _ _ _ _ = I
    1.30 -fun add_fact_nonmonotonic_types ctxt level ({kind, combformula, ...}
    1.31 +  | add_combterm_nonmonotonic_types _ _ _ _ _ = I
    1.32 +fun add_fact_nonmonotonic_types ctxt level ({kind, locality, combformula, ...}
    1.33                                              : translated_formula) =
    1.34    formula_fold (SOME (kind <> Conjecture))
    1.35 -               (add_combterm_nonmonotonic_types ctxt level) combformula
    1.36 +               (add_combterm_nonmonotonic_types ctxt level locality) combformula
    1.37  fun nonmonotonic_types_for_facts ctxt type_sys facts =
    1.38    let val level = level_of_type_sys type_sys in
    1.39      if level = Nonmonotonic_Types orelse level = Finite_Types then