merged
authorbulwahn
Wed Sep 07 14:58:40 2011 +0200 (2011-09-07)
changeset 44797e0da66339e47
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.167    K (add_iterm_syms_to_table ctxt explicit_apply)
   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.11 +        else metis_ad_hoc_type_tag, true))]
    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
   10.23 +   read correctly. *)
   10.24 +val implode_param = strip_spaces_except_between_idents o space_implode " "
   10.25  
   10.26  structure Data = Theory_Data
   10.27  (