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