--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Mon Dec 16 20:43:04 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Mon Dec 16 23:05:16 2013 +0100
@@ -19,9 +19,7 @@
Failed_to_Play of reconstructor
type minimize_command = string list -> string
-
- type one_line_params =
- play * string * (string * stature) list * minimize_command * int * int
+ type one_line_params = play * string * (string * stature) list * minimize_command * int * int
val smtN : string
end;
@@ -41,9 +39,7 @@
Failed_to_Play of reconstructor
type minimize_command = string list -> string
-
-type one_line_params =
- play * string * (string * stature) list * minimize_command * int * int
+type one_line_params = play * string * (string * stature) list * minimize_command * int * int
val smtN = "smt"