author bulwahn Wed Sep 07 14:58:40 2011 +0200 (2011-09-07) changeset 44797 e0da66339e47 parent 44796 7f1f164696a4 parent 44787 3c0741556e19 child 44798 9900c0069ae6 child 44821 a92f65e174cf
merged
```     1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Wed Sep 07 13:51:39 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Sep 07 14:58:40 2011 +0200
1.3 @@ -236,6 +236,12 @@
1.4    | string_for_kind Hypothesis = "hypothesis"
1.5    | string_for_kind Conjecture = "conjecture"
1.6
1.7 +fun string_for_app format func args =
1.8 +  if is_format_thf format then
1.9 +    "(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")"
1.10 +  else
1.11 +    func ^ "(" ^ commas args ^ ")"
1.12 +
1.13  fun flatten_type (ATyAbs (tys, ty)) = ATyAbs (tys, flatten_type ty)
1.14    | flatten_type (ty as AFun (ty1 as AType _, ty2)) =
1.15      (case flatten_type ty2 of
1.16 @@ -247,16 +253,17 @@
1.17    | flatten_type _ =
1.18      raise Fail "unexpected higher-order type in first-order format"
1.19
1.20 -fun str_for_type ty =
1.21 +fun str_for_type format ty =
1.22    let
1.23      fun str _ (AType (s, [])) = s
1.24        | str _ (AType (s, tys)) =
1.25 -        tys |> map (str false)
1.26 -            |> (if s = tptp_product_type then
1.27 -                  space_implode (" " ^ tptp_product_type ^ " ")
1.28 -                  #> length tys > 1 ? enclose "(" ")"
1.29 -                else
1.30 -                  commas #> enclose "(" ")" #> prefix s)
1.31 +        let val ss = tys |> map (str false) in
1.32 +          if s = tptp_product_type then
1.33 +            ss |> space_implode (" " ^ tptp_product_type ^ " ")
1.34 +               |> length ss > 1 ? enclose "(" ")"
1.35 +          else
1.36 +            string_for_app format s ss
1.37 +        end
1.38        | str rhs (AFun (ty1, ty2)) =
1.39          str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2
1.40          |> not rhs ? enclose "(" ")"
1.41 @@ -266,8 +273,8 @@
1.42                      ss) ^ "]: " ^ str false ty
1.43    in str true ty end
1.44
1.45 -fun string_for_type (THF _) ty = str_for_type ty
1.46 -  | string_for_type (TFF _) ty = str_for_type (flatten_type ty)
1.47 +fun string_for_type (format as THF _) ty = str_for_type format ty
1.48 +  | string_for_type (format as TFF _) ty = str_for_type format (flatten_type ty)
1.49    | string_for_type _ _ = raise Fail "unexpected type in untyped format"
1.50
1.51  fun string_for_quantifier AForall = tptp_forall
1.52 @@ -293,35 +300,27 @@
1.53
1.54  fun string_for_term _ (ATerm (s, [])) = s
1.55    | string_for_term format (ATerm (s, ts)) =
1.56 -    if s = tptp_empty_list then
1.57 -      (* used for lists in the optional "source" field of a derivation *)
1.58 -      "[" ^ commas (map (string_for_term format) ts) ^ "]"
1.59 -    else if is_tptp_equal s then
1.60 -      space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
1.61 -      |> is_format_thf format ? enclose "(" ")"
1.62 -    else
1.63 -      (case (s = tptp_ho_forall orelse s = tptp_ho_exists,
1.64 -             s = tptp_choice andalso is_format_with_choice format, ts) of
1.65 -         (true, _, [AAbs ((s', ty), tm)]) =>
1.66 -         (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
1.67 -            possible, to work around LEO-II 1.2.8 parser limitation. *)
1.68 -         string_for_formula format
1.69 -             (AQuant (if s = tptp_ho_forall then AForall else AExists,
1.70 -                      [(s', SOME ty)], AAtom tm))
1.71 -       | (_, true, [AAbs ((s', ty), tm)]) =>
1.72 -         (* There is code in "ATP_Translate" to ensure that "Eps" is always
1.73 -            applied to an abstraction. *)
1.74 -         tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
1.75 -           string_for_term format tm ^ ""
1.76 -         |> enclose "(" ")"
1.77 -
1.78 -       | _ =>
1.79 -         let val ss = map (string_for_term format) ts in
1.80 -           if is_format_thf format then
1.81 -             "(" ^ space_implode (" " ^ tptp_app ^ " ") (s :: ss) ^ ")"
1.82 -           else
1.83 -             s ^ "(" ^ commas ss ^ ")"
1.84 -         end)
1.85 +    (if s = tptp_empty_list then
1.86 +       (* used for lists in the optional "source" field of a derivation *)
1.87 +       "[" ^ commas (map (string_for_term format) ts) ^ "]"
1.88 +     else if is_tptp_equal s then
1.89 +       space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
1.90 +       |> is_format_thf format ? enclose "(" ")"
1.91 +     else case (s = tptp_ho_forall orelse s = tptp_ho_exists,
1.92 +                s = tptp_choice andalso is_format_with_choice format, ts) of
1.93 +       (true, _, [AAbs ((s', ty), tm)]) =>
1.94 +       (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
1.95 +          possible, to work around LEO-II 1.2.8 parser limitation. *)
1.96 +       string_for_formula format
1.97 +           (AQuant (if s = tptp_ho_forall then AForall else AExists,
1.98 +                    [(s', SOME ty)], AAtom tm))
1.99 +     | (_, true, [AAbs ((s', ty), tm)]) =>
1.100 +       (* There is code in "ATP_Translate" to ensure that "Eps" is always
1.101 +          applied to an abstraction. *)
1.102 +       tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
1.103 +         string_for_term format tm ^ ""
1.104 +       |> enclose "(" ")"
1.105 +     | _ => string_for_app format s (map (string_for_term format) ts))
1.106    | string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
1.107      "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^
1.108      string_for_term format tm ^ ")"
```
```     2.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Sep 07 13:51:39 2011 +0200
2.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Sep 07 14:58:40 2011 +0200
2.3 @@ -92,9 +92,6 @@
2.4    InternalError |
2.5    UnknownError of string
2.6
2.7 -fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
2.8 -val strip_spaces_except_between_ident_chars = strip_spaces true is_ident_char
2.9 -
2.10  fun elide_string threshold s =
2.11    if size s > threshold then
2.12      String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^
2.13 @@ -475,7 +472,7 @@
2.14  fun parse_line problem spass_names =
2.15    parse_tstp_line problem || parse_spass_line spass_names
2.16  fun parse_proof problem spass_names tstp =
2.17 -  tstp |> strip_spaces_except_between_ident_chars
2.18 +  tstp |> strip_spaces_except_between_idents
2.19         |> raw_explode
2.20         |> Scan.finite Symbol.stopper
2.21                (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
```
```     3.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Sep 07 13:51:39 2011 +0200
3.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Sep 07 14:58:40 2011 +0200
3.3 @@ -152,7 +152,7 @@
3.4      union (op =) (resolve_fact facts_offset fact_names name)
3.5    | add_fact ctxt _ _ (Inference (_, _, deps)) =
3.6      if AList.defined (op =) deps leo2_ext then
3.7 -      insert (op =) (ext_name ctxt, Extensionality)
3.8 +      insert (op =) (ext_name ctxt, General)
3.9      else
3.10        I
3.11    | add_fact _ _ _ _ = I
```
```     4.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Sep 07 13:51:39 2011 +0200
4.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Sep 07 14:58:40 2011 +0200
4.3 @@ -403,11 +403,11 @@
4.4     prem_kind = Hypothesis,
4.5     best_slices = K [(1.0, (false, (200, format, type_enc, "")))]}
4.6
4.7 -val pff_format = TFF (TPTP_Polymorphic, TPTP_Implicit)
4.8 +val pff_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
4.9  val pff_config = dummy_config pff_format "poly_simple"
4.10  val pff = (pffN, pff_config)
4.11
4.12 -val phf_format = THF (TPTP_Polymorphic, TPTP_Implicit, THF_With_Choice)
4.13 +val phf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice)
4.14  val phf_config = dummy_config phf_format "poly_simple_higher"
4.15  val phf = (phfN, phf_config)
4.16
```
```     5.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 13:51:39 2011 +0200
5.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 14:58:40 2011 +0200
5.3 @@ -16,24 +16,18 @@
5.4    type 'a problem = 'a ATP_Problem.problem
5.5
5.6    datatype locality =
5.7 -    General | Helper | Induction | Extensionality | Intro | Elim | Simp |
5.8 -    Local | Assum | Chained
5.9 +    General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
5.10
5.11 -  datatype order = First_Order | Higher_Order
5.12    datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
5.13    datatype soundness = Sound_Modulo_Infiniteness | Sound
5.14 -  datatype uniformity = Uniform | Nonuniform
5.15 +  datatype heaviness = Heavy | Ann_Light | Arg_Light
5.16    datatype type_level =
5.17      All_Types |
5.18 -    Noninf_Nonmono_Types of soundness * uniformity |
5.19 -    Fin_Nonmono_Types of uniformity |
5.20 +    Noninf_Nonmono_Types of soundness * heaviness |
5.21 +    Fin_Nonmono_Types of heaviness |
5.22      Const_Arg_Types |
5.23      No_Types
5.24 -
5.25 -  datatype type_enc =
5.26 -    Simple_Types of order * polymorphism * type_level |
5.27 -    Guards of polymorphism * type_level |
5.28 -    Tags of polymorphism * type_level
5.29 +  type type_enc
5.30
5.31    val type_tag_idempotence : bool Config.T
5.32    val type_tag_arguments : bool Config.T
5.33 @@ -531,17 +525,16 @@
5.34      in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end
5.35
5.36  datatype locality =
5.37 -  General | Helper | Induction | Extensionality | Intro | Elim | Simp |
5.38 -  Local | Assum | Chained
5.39 +  General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
5.40
5.41  datatype order = First_Order | Higher_Order
5.42  datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
5.43  datatype soundness = Sound_Modulo_Infiniteness | Sound
5.44 -datatype uniformity = Uniform | Nonuniform
5.45 +datatype heaviness = Heavy | Ann_Light | Arg_Light
5.46  datatype type_level =
5.47    All_Types |
5.48 -  Noninf_Nonmono_Types of soundness * uniformity |
5.49 -  Fin_Nonmono_Types of uniformity |
5.50 +  Noninf_Nonmono_Types of soundness * heaviness |
5.51 +  Fin_Nonmono_Types of heaviness |
5.52    Const_Arg_Types |
5.53    No_Types
5.54
5.55 @@ -561,9 +554,9 @@
5.56    | level_of_type_enc (Guards (_, level)) = level
5.57    | level_of_type_enc (Tags (_, level)) = level
5.58
5.59 -fun is_level_uniform (Noninf_Nonmono_Types (_, Nonuniform)) = false
5.60 -  | is_level_uniform (Fin_Nonmono_Types Nonuniform) = false
5.61 -  | is_level_uniform _ = true
5.62 +fun heaviness_of_level (Noninf_Nonmono_Types (_, heaviness)) = heaviness
5.63 +  | heaviness_of_level (Fin_Nonmono_Types heaviness) = heaviness
5.64 +  | heaviness_of_level _ = Heavy
5.65
5.66  fun is_type_level_quasi_sound All_Types = true
5.67    | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
5.68 @@ -578,11 +571,25 @@
5.69    | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true
5.70    | is_type_level_monotonicity_based _ = false
5.71
5.72 +(* "_query", "_bang", and "_at" are for the ASCII-challenged Metis and
5.73 +   Mirabelle. *)
5.74 +val queries = ["?", "_query"]
5.75 +val bangs = ["!", "_bang"]
5.76 +val ats = ["@", "_at"]
5.77 +
5.78  fun try_unsuffixes ss s =
5.79    fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
5.80
5.81 -val queries = ["?", "_query"]
5.82 -val bangs = ["!", "_bang"]
5.83 +fun try_nonmono constr suffixes fallback s =
5.84 +  case try_unsuffixes suffixes s of
5.85 +    SOME s =>
5.86 +    (case try_unsuffixes suffixes s of
5.87 +       SOME s => (constr Ann_Light, s)
5.88 +     | NONE =>
5.89 +       case try_unsuffixes ats s of
5.90 +         SOME s => (constr Arg_Light, s)
5.91 +       | NONE => (constr Heavy, s))
5.92 +  | NONE => fallback s
5.93
5.94  fun type_enc_from_string soundness s =
5.95    (case try (unprefix "poly_") s of
5.96 @@ -594,21 +601,9 @@
5.97         case try (unprefix "mono_") s of
5.98           SOME s => (SOME Mangled_Monomorphic, s)
5.99         | NONE => (NONE, s))
5.100 -  ||> (fn s =>
5.101 -          (* "_query" and "_bang" are for the ASCII-challenged Metis and
5.102 -             Mirabelle. *)
5.103 -          case try_unsuffixes queries s of
5.104 -            SOME s =>
5.105 -            (case try_unsuffixes queries s of
5.106 -               SOME s => (Noninf_Nonmono_Types (soundness, Nonuniform), s)
5.107 -             | NONE => (Noninf_Nonmono_Types (soundness, Uniform), s))
5.108 -          | NONE =>
5.109 -            case try_unsuffixes bangs s of
5.110 -              SOME s =>
5.111 -              (case try_unsuffixes bangs s of
5.112 -                 SOME s => (Fin_Nonmono_Types Nonuniform, s)
5.113 -               | NONE => (Fin_Nonmono_Types Uniform, s))
5.114 -            | NONE => (All_Types, s))
5.115 +  ||> (pair All_Types
5.116 +       |> try_nonmono Fin_Nonmono_Types bangs
5.117 +       |> try_nonmono (curry Noninf_Nonmono_Types soundness) queries)
5.118    |> (fn (poly, (level, core)) =>
5.119           case (core, (poly, level)) of
5.120             ("simple", (SOME poly, _)) =>
5.121 @@ -616,7 +611,7 @@
5.122                (Polymorphic, All_Types) =>
5.123                Simple_Types (First_Order, Polymorphic, All_Types)
5.124              | (Mangled_Monomorphic, _) =>
5.125 -              if is_level_uniform level then
5.126 +              if heaviness_of_level level = Heavy then
5.127                  Simple_Types (First_Order, Mangled_Monomorphic, level)
5.128                else
5.129                  raise Same.SAME
5.130 @@ -627,7 +622,7 @@
5.131                Simple_Types (Higher_Order, Polymorphic, All_Types)
5.132              | (_, Noninf_Nonmono_Types _) => raise Same.SAME
5.133              | (Mangled_Monomorphic, _) =>
5.134 -              if is_level_uniform level then
5.135 +              if heaviness_of_level level = Heavy then
5.136                  Simple_Types (Higher_Order, Mangled_Monomorphic, level)
5.137                else
5.138                  raise Same.SAME
5.139 @@ -640,7 +635,7 @@
5.140           | ("erased", (NONE, All_Types (* naja *))) =>
5.141             Guards (Polymorphic, No_Types)
5.142           | _ => raise Same.SAME)
5.143 -  handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
5.144 +  handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")
5.145
5.146  fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
5.147                      (Simple_Types (order, _, level)) =
5.148 @@ -1241,7 +1236,7 @@
5.149    | should_encode_type _ _ _ _ = false
5.150
5.151  fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
5.152 -    (is_level_uniform level orelse should_guard_var ()) andalso
5.153 +    (heaviness_of_level level = Heavy orelse should_guard_var ()) andalso
5.154      should_encode_type ctxt mono level T
5.155    | should_guard_type _ _ _ _ _ = false
5.156
5.157 @@ -1258,7 +1253,7 @@
5.158
5.159  fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
5.160    | should_tag_with_type ctxt mono (Tags (_, level)) site u T =
5.161 -    (if is_level_uniform level then
5.162 +    (if heaviness_of_level level = Heavy then
5.163         should_encode_type ctxt mono level T
5.164       else case (site, is_maybe_universal_var u) of
5.165         (Eq_Arg _, true) => should_encode_type ctxt mono level T
5.166 @@ -1366,21 +1361,21 @@
5.168    |> formula_fold NONE |> fact_lift
5.169
5.170 -val default_sym_tab_entries : (string * sym_info) list =
5.171 -  (prefixed_predicator_name,
5.172 -   {pred_sym = true, min_ary = 1, max_ary = 1, types = []})
5.173 -       (* FIXME: needed? *) ::
5.174 +fun default_sym_tab_entries type_enc =
5.175    (make_fixed_const NONE @{const_name undefined},
5.176 -   {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
5.177 +                   {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
5.178    ([tptp_false, tptp_true]
5.179     |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
5.180    ([tptp_equal, tptp_old_equal]
5.181     |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
5.182 +  |> not (is_type_enc_higher_order type_enc)
5.183 +     ? cons (prefixed_predicator_name,
5.184 +             {pred_sym = true, min_ary = 1, max_ary = 1, types = []})
5.185
5.186 -fun sym_table_for_facts ctxt explicit_apply facts =
5.187 +fun sym_table_for_facts ctxt type_enc explicit_apply facts =
5.188    ((false, []), Symtab.empty)
5.189    |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
5.190 -  |> fold Symtab.update default_sym_tab_entries
5.191 +  |> fold Symtab.update (default_sym_tab_entries type_enc)
5.192
5.193  fun min_ary_of sym_tab s =
5.194    case Symtab.lookup sym_tab s of
5.195 @@ -1657,7 +1652,8 @@
5.196
5.197  fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
5.198    | should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T =
5.199 -    not (is_level_uniform level) andalso should_encode_type ctxt mono level T
5.200 +    heaviness_of_level level <> Heavy andalso
5.201 +    should_encode_type ctxt mono level T
5.202    | should_generate_tag_bound_decl _ _ _ _ _ = false
5.203
5.204  fun mk_aterm format type_enc name T_args args =
5.205 @@ -1877,8 +1873,8 @@
5.206         ? (fold (add_fact_syms true) conjs
5.207            #> fold (add_fact_syms false) facts
5.208            #> (case type_enc of
5.209 -                Simple_Types (_, poly, _) =>
5.210 -                if poly = Polymorphic then add_TYPE_const () else I
5.211 +                Simple_Types (First_Order, Polymorphic, _) => add_TYPE_const ()
5.212 +              | Simple_Types _ => I
5.213                | _ => fold add_undefined_const (var_types ())))
5.214    end
5.215
5.216 @@ -2131,7 +2127,7 @@
5.217                                                   type_enc n s)
5.218      end
5.219    | Tags (_, level) =>
5.220 -    if is_level_uniform level then
5.221 +    if heaviness_of_level level = Heavy then
5.222        []
5.223      else
5.224        let val n = length decls in
5.225 @@ -2209,11 +2205,13 @@
5.226      val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses) =
5.227        translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
5.228                           hyp_ts concl_t facts
5.229 -    val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
5.230 +    val sym_tab =
5.231 +      conjs @ facts |> sym_table_for_facts ctxt type_enc explicit_apply
5.232      val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
5.233      val firstorderize = firstorderize_fact thy format type_enc sym_tab
5.234      val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize)
5.235 -    val sym_tab = conjs @ facts |> sym_table_for_facts ctxt (SOME false)
5.236 +    val sym_tab =
5.237 +      conjs @ facts |> sym_table_for_facts ctxt type_enc (SOME false)
5.238      val helpers =
5.239        sym_tab |> helper_facts_for_sym_table ctxt format type_enc
5.240                |> map firstorderize
```
```     6.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Wed Sep 07 13:51:39 2011 +0200
6.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Wed Sep 07 14:58:40 2011 +0200
6.3 @@ -10,6 +10,7 @@
6.4    val hash_string : string -> int
6.5    val hash_term : term -> int
6.6    val strip_spaces : bool -> (char -> bool) -> string -> string
6.7 +  val strip_spaces_except_between_idents : string -> string
6.8    val nat_subscript : int -> string
6.9    val unyxml : string -> string
6.10    val maybe_quote : string -> string
6.11 @@ -88,6 +89,9 @@
6.12  fun strip_spaces skip_comments is_evil =
6.13    implode o strip_spaces_in_list skip_comments is_evil o String.explode
6.14
6.15 +fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
6.16 +val strip_spaces_except_between_idents = strip_spaces true is_ident_char
6.17 +
6.18  val subscript = implode o map (prefix "\<^isub>") o raw_explode  (* FIXME Symbol.explode (?) *)
6.19  fun nat_subscript n =
6.20    n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
```
```     7.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Wed Sep 07 13:51:39 2011 +0200
7.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Wed Sep 07 14:58:40 2011 +0200
7.3 @@ -59,8 +59,9 @@
7.4     ((prefixed_predicator_name, 1), (K metis_predicator, false)),
7.5     ((prefixed_app_op_name, 2), (K metis_app_op, false)),
7.6     ((prefixed_type_tag_name, 2),
7.7 -    (fn Tags (_, All_Types) => metis_systematic_type_tag
7.8 -      | _ => metis_ad_hoc_type_tag, true))]
7.9 +    (fn type_enc =>
7.10 +        if level_of_type_enc type_enc = All_Types then metis_systematic_type_tag
7.12
7.13  fun old_skolem_const_name i j num_T_args =
7.14    old_skolem_const_prefix ^ Long_Name.separator ^
```
```     8.1 --- a/src/HOL/Tools/Nitpick/nitrox.ML	Wed Sep 07 13:51:39 2011 +0200
8.2 +++ b/src/HOL/Tools/Nitpick/nitrox.ML	Wed Sep 07 14:58:40 2011 +0200
8.3 @@ -21,8 +21,7 @@
8.4
8.5  exception SYNTAX of string
8.6
8.7 -fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
8.8 -val tptp_explode = raw_explode o strip_spaces true is_ident_char
8.9 +val tptp_explode = raw_explode o strip_spaces_except_between_idents
8.10
8.11  fun parse_file_path (c :: ss) =
8.12      if c = "'" orelse c = "\"" then
```
```     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 07 13:51:39 2011 +0200
9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 07 14:58:40 2011 +0200
9.3 @@ -144,7 +144,6 @@
9.4                   (j + 1,
9.5                    ((nth_name j,
9.6                      if member Thm.eq_thm_prop chained_ths th then Chained
9.7 -                    else if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
9.8                      else General), th) :: rest))
9.9      |> snd
9.10    end
9.11 @@ -576,7 +575,7 @@
9.12          | _ => SOME tab
9.13    in aux (prop_of th) [] end
9.14
9.15 -(* FIXME: This is currently only useful for polymorphic type systems. *)
9.16 +(* FIXME: This is currently only useful for polymorphic type encodings. *)
9.17  fun could_benefit_from_ext is_built_in_const facts =
9.18    fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty)
9.19    |> is_none
9.20 @@ -845,8 +844,7 @@
9.21        else if global then
9.22          case Termtab.lookup clasimpset_table (prop_of th) of
9.23            SOME loc => loc
9.24 -        | NONE => if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
9.25 -                  else General
9.26 +        | NONE => General
9.27        else if is_assum th then Assum else Local
9.28      fun is_good_unnamed_local th =
9.29        not (Thm.has_name_hint th) andalso
```
```    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 07 13:51:39 2011 +0200
10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 07 14:58:40 2011 +0200
10.3 @@ -19,6 +19,7 @@
10.4  structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
10.5  struct
10.6
10.7 +open ATP_Util
10.8  open ATP_Systems
10.9  open ATP_Translate
10.10  open Sledgehammer_Util
10.11 @@ -151,13 +152,9 @@
10.12             error ("Unknown parameter: " ^ quote name ^ "."))
10.13
10.14
10.15 -(* Ensure that type systems such as "mono_simple?" and "mono_guards!!" are
10.16 -   handled correctly. *)
10.17 -fun implode_param [s, "?"] = s ^ "?"
10.18 -  | implode_param [s, "??"] = s ^ "??"
10.19 -  | implode_param [s, "!"] = s ^ "!"
10.20 -  | implode_param [s, "!!"] = s ^ "!!"
10.21 -  | implode_param ss = space_implode " " ss
10.22 +(* Ensures that type encodings such as "mono_simple?" and "poly_guards!!" are