1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 13:50:17 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 13:50:17 2011 +0200
     1.3 @@ -571,11 +571,25 @@
     1.4    | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true
     1.5    | is_type_level_monotonicity_based _ = false
     1.6  
     1.7 +(* "_query", "_bang", and "_at" are for the ASCII-challenged Metis and
     1.8 +   Mirabelle. *)
     1.9 +val queries = ["?", "_query"]
    1.10 +val bangs = ["!", "_bang"]
    1.11 +val ats = ["@", "_at"]
    1.12 +
    1.13  fun try_unsuffixes ss s =
    1.14    fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
    1.15  
    1.16 -val queries = ["?", "_query"]
    1.17 -val bangs = ["!", "_bang"]
    1.18 +fun try_nonmono constr suffixes fallback s =
    1.19 +  case try_unsuffixes suffixes s of
    1.20 +    SOME s =>
    1.21 +    (case try_unsuffixes suffixes s of
    1.22 +       SOME s => (constr Ann_Light, s)
    1.23 +     | NONE =>
    1.24 +       case try_unsuffixes ats s of
    1.25 +         SOME s => (constr Arg_Light, s)
    1.26 +       | NONE => (constr Heavy, s))
    1.27 +  | NONE => fallback s
    1.28  
    1.29  fun type_enc_from_string soundness s =
    1.30    (case try (unprefix "poly_") s of
    1.31 @@ -587,21 +601,9 @@
    1.32         case try (unprefix "mono_") s of
    1.33           SOME s => (SOME Mangled_Monomorphic, s)
    1.34         | NONE => (NONE, s))
    1.35 -  ||> (fn s =>
    1.36 -          (* "_query" and "_bang" are for the ASCII-challenged Metis and
    1.37 -             Mirabelle. *)
    1.38 -          case try_unsuffixes queries s of
    1.39 -            SOME s =>
    1.40 -            (case try_unsuffixes queries s of
    1.41 -               SOME s => (Noninf_Nonmono_Types (soundness, Ann_Light), s)
    1.42 -             | NONE => (Noninf_Nonmono_Types (soundness, Heavy), s))
    1.43 -          | NONE =>
    1.44 -            case try_unsuffixes bangs s of
    1.45 -              SOME s =>
    1.46 -              (case try_unsuffixes bangs s of
    1.47 -                 SOME s => (Fin_Nonmono_Types Ann_Light, s)
    1.48 -               | NONE => (Fin_Nonmono_Types Heavy, s))
    1.49 -            | NONE => (All_Types, s))
    1.50 +  ||> (pair All_Types
    1.51 +       |> try_nonmono Fin_Nonmono_Types bangs
    1.52 +       |> try_nonmono (curry Noninf_Nonmono_Types soundness) queries)
    1.53    |> (fn (poly, (level, core)) =>
    1.54           case (core, (poly, level)) of
    1.55             ("simple", (SOME poly, _)) =>
    1.56 @@ -633,7 +635,7 @@
    1.57           | ("erased", (NONE, All_Types (* naja *))) =>
    1.58             Guards (Polymorphic, No_Types)
    1.59           | _ => raise Same.SAME)
    1.60 -  handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
    1.61 +  handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")
    1.62  
    1.63  fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
    1.64                      (Simple_Types (order, _, level)) =

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 07 13:50:17 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 07 13:50:17 2011 +0200
     2.3 @@ -575,7 +575,7 @@
     2.4          | _ => SOME tab
     2.5    in aux (prop_of th) [] end
     2.6  
     2.7 -(* FIXME: This is currently only useful for polymorphic type systems. *)
     2.8 +(* FIXME: This is currently only useful for polymorphic type encodings. *)
     2.9  fun could_benefit_from_ext is_built_in_const facts =
    2.10    fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty)
    2.11    |> is_none

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 07 13:50:17 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 07 13:50:17 2011 +0200
     3.3 @@ -152,8 +152,8 @@
     3.4             error ("Unknown parameter: " ^ quote name ^ "."))
     3.5  
     3.6  
     3.7 -(* Ensure that type systems such as "mono_simple?" and "poly_guards!!" are
     3.8 -   handled correctly. *)
     3.9 +(* Ensures that type encodings such as "mono_simple?" and "poly_guards!!" are
    3.10 +   read correctly. *)
    3.11  val implode_param = strip_spaces_except_between_idents o space_implode " "
    3.12  
    3.13  structure Data = Theory_Data