--- 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))
--- 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
--- 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
--- 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
--- 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,