# HG changeset patch
# User blanchet
# Date 1306852716 -7200
# Node ID 9a42899ec16906e166c77870b2244234c6685a10
# Parent  1d46d85cd78bfa6f3bb08cbda07208181d257fda
tuned name

diff -r 1d46d85cd78b -r 9a42899ec169 src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Tue May 31 16:38:36 2011 +0200
@@ -11,7 +11,7 @@
   type 'a fo_term = 'a ATP_Problem.fo_term
   type 'a proof = 'a ATP_Proof.proof
   type locality = ATP_Translate.locality
-  type type_system = ATP_Translate.type_system
+  type type_sys = ATP_Translate.type_sys
 
   datatype reconstructor =
     Metis |
@@ -27,18 +27,17 @@
   type one_line_params =
     play * string * (string * locality) list * minimize_command * int * int
   type isar_params =
-    bool * bool * int * type_system * string Symtab.table * int list list
-    * int * (string * locality) list vector * int Symtab.table * string proof
-    * thm
+    bool * bool * int * type_sys * string Symtab.table * int list list * int
+    * (string * locality) list vector * int Symtab.table * string proof * thm
   val repair_conjecture_shape_and_fact_names :
-    type_system -> string -> int list list -> int
+    type_sys -> string -> int list list -> int
     -> (string * locality) list vector -> int list
     -> int list list * int * (string * locality) list vector * int list
   val used_facts_in_atp_proof :
-    Proof.context -> type_system -> int -> (string * locality) list vector
+    Proof.context -> type_sys -> int -> (string * locality) list vector
     -> string proof -> (string * locality) list
   val used_facts_in_unsound_atp_proof :
-    Proof.context -> type_system -> int list list -> int
+    Proof.context -> type_sys -> int list list -> int
     -> (string * locality) list vector -> 'a proof -> string list option
   val uses_typed_helpers : int list -> 'a proof -> bool
   val reconstructor_name : reconstructor -> string
@@ -74,7 +73,7 @@
 type one_line_params =
   play * string * (string * locality) list * minimize_command * int * int
 type isar_params =
-  bool * bool * int * type_system * string Symtab.table * int list list * int
+  bool * bool * int * type_sys * string Symtab.table * int list list * int
   * (string * locality) list vector * int Symtab.table * string proof * thm
 
 fun is_head_digit s = Char.isDigit (String.sub (s, 0))
diff -r 1d46d85cd78b -r 9a42899ec169 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue May 31 16:38:36 2011 +0200
@@ -45,7 +45,7 @@
     All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
   datatype type_heaviness = Heavy | Light
 
-  datatype type_system =
+  datatype type_sys =
     Simple_Types of type_level |
     Preds of polymorphism * type_level * type_heaviness |
     Tags of polymorphism * type_level * type_heaviness
@@ -98,23 +98,23 @@
   val combterm_from_term :
     theory -> (string * typ) list -> term -> combterm * typ list
   val is_locality_global : locality -> bool
-  val type_sys_from_string : string -> type_system
-  val polymorphism_of_type_sys : type_system -> polymorphism
-  val level_of_type_sys : type_system -> type_level
-  val is_type_sys_virtually_sound : type_system -> bool
-  val is_type_sys_fairly_sound : type_system -> bool
-  val choose_format : format list -> type_system -> format * type_system
+  val type_sys_from_string : string -> type_sys
+  val polymorphism_of_type_sys : type_sys -> polymorphism
+  val level_of_type_sys : type_sys -> type_level
+  val is_type_sys_virtually_sound : type_sys -> bool
+  val is_type_sys_fairly_sound : type_sys -> bool
+  val choose_format : format list -> type_sys -> format * type_sys
   val raw_type_literals_for_types : typ list -> type_literal list
   val unmangled_const : string -> string * string fo_term list
   val translate_atp_fact :
-    Proof.context -> format -> type_system -> bool -> (string * locality) * thm
+    Proof.context -> format -> type_sys -> bool -> (string * locality) * thm
     -> translated_formula option * ((string * locality) * thm)
   val helper_table : (string * (bool * thm list)) list
   val tfree_classes_of_terms : term list -> string list
   val tvar_classes_of_terms : term list -> string list
   val type_consts_of_terms : theory -> term list -> string list
   val prepare_atp_problem :
-    Proof.context -> format -> formula_kind -> formula_kind -> type_system
+    Proof.context -> format -> formula_kind -> formula_kind -> type_sys
     -> bool option -> bool -> bool -> term list -> term
     -> (translated_formula option * ((string * 'a) * thm)) list
     -> string problem * string Symtab.table * int * int
@@ -498,7 +498,7 @@
   All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
 datatype type_heaviness = Heavy | Light
 
-datatype type_system =
+datatype type_sys =
   Simple_Types of type_level |
   Preds of polymorphism * type_level * type_heaviness |
   Tags of polymorphism * type_level * type_heaviness
diff -r 1d46d85cd78b -r 9a42899ec169 src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Tue May 31 16:38:36 2011 +0200
@@ -9,7 +9,7 @@
 
 signature METIS_TACTICS =
 sig
-  type type_system = ATP_Translate.type_system
+  type type_sys = ATP_Translate.type_sys
 
   val metisN : string
   val metisF_N : string
@@ -22,8 +22,7 @@
   val metisF_tac : Proof.context -> thm list -> int -> tactic
   val metisFT_tac : Proof.context -> thm list -> int -> tactic
   val metisHO_tac : Proof.context -> thm list -> int -> tactic
-  val metisX_tac :
-    Proof.context -> type_system option -> thm list -> int -> tactic
+  val metisX_tac : Proof.context -> type_sys option -> thm list -> int -> tactic
   val setup : theory -> theory
 end
 
diff -r 1d46d85cd78b -r 9a42899ec169 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue May 31 16:38:36 2011 +0200
@@ -10,7 +10,7 @@
 signature METIS_TRANSLATE =
 sig
   type type_literal = ATP_Translate.type_literal
-  type type_system = ATP_Translate.type_system
+  type type_sys = ATP_Translate.type_sys
 
   datatype mode = FO | HO | FT | New
 
@@ -27,7 +27,7 @@
   val reveal_old_skolem_terms : (string * term) list -> term -> term
   val string_of_mode : mode -> string
   val prepare_metis_problem :
-    Proof.context -> mode -> type_system option -> thm list -> thm list
+    Proof.context -> mode -> type_sys option -> thm list -> thm list
     -> mode * int Symtab.table * metis_problem
 end
 
diff -r 1d46d85cd78b -r 9a42899ec169 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 31 16:38:36 2011 +0200
@@ -12,14 +12,14 @@
   type locality = ATP_Translate.locality
   type relevance_fudge = Sledgehammer_Filter.relevance_fudge
   type translated_formula = ATP_Translate.translated_formula
-  type type_system = ATP_Translate.type_system
+  type type_sys = ATP_Translate.type_sys
   type play = ATP_Reconstruct.play
   type minimize_command = ATP_Reconstruct.minimize_command
 
   datatype mode = Auto_Try | Try | Normal | Minimize
 
-  datatype rich_type_system =
-    Dumb_Type_Sys of type_system |
+  datatype rich_type_sys =
+    Dumb_Type_Sys of type_sys |
     Smart_Type_Sys of bool
 
   type params =
@@ -28,7 +28,7 @@
      overlord: bool,
      blocking: bool,
      provers: string list,
-     type_sys: rich_type_system,
+     type_sys: rich_type_sys,
      relevance_thresholds: real * real,
      max_relevant: int option,
      max_mono_iters: int,
@@ -288,8 +288,8 @@
 
 (** problems, results, ATPs, etc. **)
 
-datatype rich_type_system =
-  Dumb_Type_Sys of type_system |
+datatype rich_type_sys =
+  Dumb_Type_Sys of type_sys |
   Smart_Type_Sys of bool
 
 type params =
@@ -298,7 +298,7 @@
    overlord: bool,
    blocking: bool,
    provers: string list,
-   type_sys: rich_type_system,
+   type_sys: rich_type_sys,
    relevance_thresholds: real * real,
    max_relevant: int option,
    max_mono_iters: int,