tuned names

--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 01 10:29:43 2011 +0200
@@ -43,7 +43,7 @@
   datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
   datatype type_level =
     All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
-  datatype type_heaviness = Heavy | Light
+  datatype type_heaviness = Heavyweight | Lightweight
 
   datatype type_sys =
     Simple_Types of type_level |
@@ -504,7 +504,7 @@
 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
 datatype type_level =
   All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
-datatype type_heaviness = Heavy | Light
+datatype type_heaviness = Heavyweight | Lightweight
 
 datatype type_sys =
   Simple_Types of type_level |
@@ -534,22 +534,22 @@
             | NONE => (All_Types, s))
   ||> apsnd (fn s =>
                 case try (unsuffix "_heavy") s of
-                  SOME s => (Heavy, s)
-                | NONE => (Light, s))
+                  SOME s => (Heavyweight, s)
+                | NONE => (Lightweight, s))
   |> (fn (poly, (level, (heaviness, core))) =>
          case (core, (poly, level, heaviness)) of
-           ("simple", (NONE, _, Light)) => Simple_Types level
+           ("simple", (NONE, _, Lightweight)) => Simple_Types level
          | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
          | ("tags", (SOME Polymorphic, All_Types, _)) =>
            Tags (Polymorphic, All_Types, heaviness)
          | ("tags", (SOME Polymorphic, _, _)) =>
            (* The actual light encoding is very unsound. *)
-           Tags (Polymorphic, level, Heavy)
+           Tags (Polymorphic, level, Heavyweight)
          | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
-         | ("args", (SOME poly, All_Types (* naja *), Light)) =>
-           Preds (poly, Const_Arg_Types, Light)
-         | ("erased", (NONE, All_Types (* naja *), Light)) =>
-           Preds (Polymorphic, No_Types, Light)
+         | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
+           Preds (poly, Const_Arg_Types, Lightweight)
+         | ("erased", (NONE, All_Types (* naja *), Lightweight)) =>
+           Preds (Polymorphic, No_Types, Lightweight)
          | _ => raise Same.SAME)
   handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
 
@@ -561,7 +561,7 @@
   | level_of_type_sys (Preds (_, level, _)) = level
   | level_of_type_sys (Tags (_, level, _)) = level
 
-fun heaviness_of_type_sys (Simple_Types _) = Heavy
+fun heaviness_of_type_sys (Simple_Types _) = Heavyweight
   | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness
   | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness
 
@@ -580,7 +580,7 @@
 fun choose_format formats (Simple_Types level) =
     if member (op =) formats THF then (THF, Simple_Types level)
     else if member (op =) formats TFF then (TFF, Simple_Types level)
-    else choose_format formats (Preds (Mangled_Monomorphic, level, Heavy))
+    else choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
   | choose_format formats type_sys =
     (case hd formats of
        CNF_UEQ =>
@@ -623,9 +623,9 @@
     false (* since TFF doesn't support overloading *)
   | should_drop_arg_type_args type_sys =
     level_of_type_sys type_sys = All_Types andalso
-    heaviness_of_type_sys type_sys = Heavy
+    heaviness_of_type_sys type_sys = Heavyweight
 
-fun general_type_arg_policy (Tags (_, All_Types, Heavy)) = No_Type_Args
+fun general_type_arg_policy (Tags (_, All_Types, Heavyweight)) = No_Type_Args
   | general_type_arg_policy type_sys =
     if level_of_type_sys type_sys = No_Types then
       No_Type_Args
@@ -983,7 +983,7 @@
 
 fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
                              should_predicate_on_var T =
-    (heaviness = Heavy orelse should_predicate_on_var ()) andalso
+    (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso
     should_encode_type ctxt nonmono_Ts level T
   | should_predicate_on_type _ _ _ _ _ = false
 
@@ -997,8 +997,8 @@
 fun should_tag_with_type _ _ _ Top_Level _ _ = false
   | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site u T =
     (case heaviness of
-       Heavy => should_encode_type ctxt nonmono_Ts level T
-     | Light =>
+       Heavyweight => should_encode_type ctxt nonmono_Ts level T
+     | Lightweight =>
        case (site, is_var_or_bound_var u) of
          (Eq_Arg, true) => should_encode_type ctxt nonmono_Ts level T
        | _ => false)
@@ -1204,7 +1204,7 @@
             if s = const_prefix ^ app_op_name andalso
                length T_args = 2 andalso
                not (is_type_sys_virtually_sound type_sys) andalso
-               heaviness_of_type_sys type_sys = Heavy then
+               heaviness_of_type_sys type_sys = Heavyweight then
               T_args |> map (homogenized_type ctxt nonmono_Ts level 0)
                      |> (fn Ts => let val T = hd Ts --> nth Ts 1 in
                                     (T --> T, tl Ts)
@@ -1560,7 +1560,7 @@
   is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
   (case type_sys of
      Simple_Types _ => true
-   | Tags (_, _, Light) => true
+   | Tags (_, _, Lightweight) => true
    | _ => not pred_sym)
 
 fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) =
@@ -1745,8 +1745,8 @@
     end
   | Tags (_, _, heaviness) =>
     (case heaviness of
-       Heavy => []
-     | Light =>
+       Heavyweight => []
+     | Lightweight =>
        let val n = length decls in
          (0 upto n - 1 ~~ decls)
          |> maps (formula_lines_for_tags_sym_decl ctxt format conj_sym_kind
@@ -1762,7 +1762,7 @@
   |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
                                                      nonmono_Ts type_sys)
 
-fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavy)) =
+fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavyweight)) =
     level = Nonmonotonic_Types orelse level = Finite_Types
   | should_add_ti_ti_helper _ = false
 

--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 01 10:29:43 2011 +0200
@@ -17,6 +17,8 @@
   val trace_msg : Proof.context -> (unit -> string) -> unit
   val verbose : bool Config.T
   val verbose_warning : Proof.context -> string -> unit
+  val hol_term_from_metis :
+    mode -> int Symtab.table -> Proof.context -> Metis_Term.term -> term
   val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
   val untyped_aconv : term -> term -> bool
   val replay_one_inference :
@@ -244,7 +246,7 @@
                    |> infer_types ctxt
       val _ = app (fn t => trace_msg ctxt
                     (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
-                              "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
+                              " of type " ^ Syntax.string_of_typ ctxt (type_of t)))
                   ts'
   in  ts'  end;
 

--- a/src/HOL/Tools/Metis/metis_tactics.ML	Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Wed Jun 01 10:29:43 2011 +0200
@@ -53,7 +53,7 @@
 
 (*Determining which axiom clauses are actually used*)
 fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
-  | used_axioms _ _ = NONE;
+  | used_axioms _ _ = NONE
 
 val clause_params =
   {ordering = Metis_KnuthBendixOrder.default,

--- a/src/HOL/Tools/Metis/metis_translate.ML	Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Wed Jun 01 10:29:43 2011 +0200
@@ -310,10 +310,16 @@
          |> Metis_Thm.axiom,
      case try (unprefix conjecture_prefix) ident of
        SOME s => Meson.make_meta_clause (nth clauses (the (Int.fromString s)))
-     | NONE => TrueI)
+     | NONE =>
+(* FIXME: missing:
+       if String.isPrefix helper_prefix then
+         ...
+       else
+*)
+       TrueI)
   | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
 
-val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Light)
+val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Lightweight)
 
 (* Function to generate metis clauses, including comb and type clauses *)
 fun prepare_metis_problem ctxt MX type_sys conj_clauses fact_clauses =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jun 01 10:29:43 2011 +0200
@@ -512,7 +512,7 @@
 val atp_important_message_keep_quotient = 10
 
 val fallback_best_type_systems =
-  [Preds (Mangled_Monomorphic, Nonmonotonic_Types, Light)]
+  [Preds (Mangled_Monomorphic, Nonmonotonic_Types, Lightweight)]
 
 fun choose_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
     choose_format formats type_sys

--- a/src/HOL/ex/tptp_export.ML	Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML	Wed Jun 01 10:29:43 2011 +0200
@@ -95,7 +95,7 @@
           (ATP_Translate.Polymorphic,
            if full_types then ATP_Translate.All_Types
            else ATP_Translate.Const_Arg_Types,
-           ATP_Translate.Heavy)
+           ATP_Translate.Heavyweight)
     val path = file_name |> Path.explode
     val _ = File.write path ""
     val facts0 = facts_of thy