1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Jun 10 17:52:09 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Jun 10 17:52:09 2011 +0200
     1.3 @@ -44,7 +44,8 @@
     1.4  
     1.5    datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
     1.6    datatype type_level =
     1.7 -    All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
     1.8 +    All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
     1.9 +    No_Types
    1.10    datatype type_heaviness = Heavyweight | Lightweight
    1.11  
    1.12    datatype type_sys =
    1.13 @@ -543,7 +544,8 @@
    1.14  
    1.15  datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
    1.16  datatype type_level =
    1.17 -  All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
    1.18 +  All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
    1.19 +  No_Types
    1.20  datatype type_heaviness = Heavyweight | Lightweight
    1.21  
    1.22  datatype type_sys =
    1.23 @@ -567,10 +569,10 @@
    1.24    ||> (fn s =>
    1.25            (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
    1.26            case try_unsuffixes ["?", "_query"] s of
    1.27 -            SOME s => (Nonmonotonic_Types, s)
    1.28 +            SOME s => (Noninf_Nonmono_Types, s)
    1.29            | NONE =>
    1.30              case try_unsuffixes ["!", "_bang"] s of
    1.31 -              SOME s => (Finite_Types, s)
    1.32 +              SOME s => (Fin_Nonmono_Types, s)
    1.33              | NONE => (All_Types, s))
    1.34    ||> apsnd (fn s =>
    1.35                  case try (unsuffix "_heavy") s of
    1.36 @@ -603,12 +605,12 @@
    1.37    | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness
    1.38  
    1.39  fun is_type_level_virtually_sound level =
    1.40 -  level = All_Types orelse level = Nonmonotonic_Types
    1.41 +  level = All_Types orelse level = Noninf_Nonmono_Types
    1.42  val is_type_sys_virtually_sound =
    1.43    is_type_level_virtually_sound o level_of_type_sys
    1.44  
    1.45  fun is_type_level_fairly_sound level =
    1.46 -  is_type_level_virtually_sound level orelse level = Finite_Types
    1.47 +  is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
    1.48  val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
    1.49  
    1.50  fun is_setting_higher_order THF (Simple_Types _) = true
    1.51 @@ -1022,7 +1024,7 @@
    1.52  fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
    1.53      exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
    1.54    | should_encode_type _ _ All_Types _ = true
    1.55 -  | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T
    1.56 +  | should_encode_type ctxt _ Fin_Nonmono_Types T = is_type_surely_finite ctxt T
    1.57    | should_encode_type _ _ _ _ = false
    1.58  
    1.59  fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
    1.60 @@ -1662,10 +1664,10 @@
    1.61                             tm2)) =
    1.62      (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
    1.63       (case level of
    1.64 -        Nonmonotonic_Types =>
    1.65 +        Noninf_Nonmono_Types =>
    1.66          not (is_locality_global locality) orelse
    1.67          not (is_type_surely_infinite ctxt known_infinite_types T)
    1.68 -      | Finite_Types => is_type_surely_finite ctxt T
    1.69 +      | Fin_Nonmono_Types => is_type_surely_finite ctxt T
    1.70        | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
    1.71    | add_combterm_nonmonotonic_types _ _ _ _ _ = I
    1.72  fun add_fact_nonmonotonic_types ctxt level ({kind, locality, combformula, ...}
    1.73 @@ -1674,7 +1676,7 @@
    1.74                 (add_combterm_nonmonotonic_types ctxt level locality) combformula
    1.75  fun nonmonotonic_types_for_facts ctxt type_sys facts =
    1.76    let val level = level_of_type_sys type_sys in
    1.77 -    if level = Nonmonotonic_Types orelse level = Finite_Types then
    1.78 +    if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
    1.79        [] |> fold (add_fact_nonmonotonic_types ctxt level) facts
    1.80           (* We must add "bool" in case the helper "True_or_False" is added
    1.81              later. In addition, several places in the code rely on the list of
    1.82 @@ -1834,7 +1836,7 @@
    1.83  fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
    1.84      poly <> Mangled_Monomorphic andalso
    1.85      ((level = All_Types andalso heaviness = Lightweight) orelse
    1.86 -     level = Nonmonotonic_Types orelse level = Finite_Types)
    1.87 +     level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types)
    1.88    | needs_type_tag_idempotence _ = false
    1.89  
    1.90  fun offset_of_heading_in_problem _ [] j = j

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jun 10 17:52:09 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jun 10 17:52:09 2011 +0200
     2.3 @@ -512,7 +512,7 @@
     2.4  val atp_important_message_keep_quotient = 10
     2.5  
     2.6  val fallback_best_type_systems =
     2.7 -  [Preds (Mangled_Monomorphic, Nonmonotonic_Types, Lightweight)]
     2.8 +  [Preds (Mangled_Monomorphic, Noninf_Nonmono_Types, Lightweight)]
     2.9  
    2.10  fun choose_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
    2.11      choose_format formats type_sys