--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Dec 17 11:12:10 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Dec 17 14:03:29 2013 +0100
@@ -50,8 +50,7 @@
Class_Decl of string * 'a * 'a list |
Type_Decl of string * 'a * int |
Sym_Decl of string * 'a * 'a atp_type |
- Datatype_Decl of string * ('a * 'a list) list * 'a atp_type
- * ('a, 'a atp_type) atp_term list * bool |
+ Datatype_Decl of string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list |
Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a |
Formula of (string * string) * atp_formula_role
* ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula
@@ -195,8 +194,7 @@
Class_Decl of string * 'a * 'a list |
Type_Decl of string * 'a * int |
Sym_Decl of string * 'a * 'a atp_type |
- Datatype_Decl of string * ('a * 'a list) list * 'a atp_type
- * ('a, 'a atp_type) atp_term list * bool |
+ Datatype_Decl of string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list |
Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a |
Formula of (string * string) * atp_formula_role
* ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula
@@ -624,9 +622,7 @@
(if null xs then "" else "[" ^ commas (map bound_tvar xs) ^ "], ") ^
typ ty
fun sort_decl xs ty cl = "sort(" ^ binder_typ xs ty ^ ", " ^ cl ^ ")."
- fun datatype_decl xs ty tms exhaust =
- "datatype(" ^ commas (binder_typ xs ty :: map term tms @
- (if exhaust then [] else ["..."])) ^ ")."
+ fun datatype_decl xs ty tms = "datatype(" ^ commas (binder_typ xs ty :: map term tms) ^ ")."
fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")."
fun formula pred (Formula ((ident, alt), kind, phi, _, info)) =
if pred kind then
@@ -674,8 +670,7 @@
else NONE
| _ => NONE) |> flat
val datatype_decls =
- filt (try (fn Datatype_Decl (_, xs, ty, tms, exhaust) =>
- datatype_decl xs ty tms exhaust)) |> flat
+ filt (try (fn Datatype_Decl (_, xs, ty, tms) => datatype_decl xs ty tms)) |> flat
val sort_decls =
filt (try (fn Class_Memb (_, xs, ty, cl) => sort_decl xs ty cl)) |> flat
val subclass_decls =
@@ -952,9 +947,9 @@
| nice_line (Sym_Decl (ident, sym, ty)) =
nice_name sym ##>> nice_type ty
#>> (fn (sym, ty) => Sym_Decl (ident, sym, ty))
- | nice_line (Datatype_Decl (ident, xs, ty, tms, exhaust)) =
+ | nice_line (Datatype_Decl (ident, xs, ty, tms)) =
nice_bound_tvars xs ##>> nice_type ty ##>> fold_map nice_term tms
- #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms, exhaust))
+ #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms))
| nice_line (Class_Memb (ident, xs, ty, cl)) =
nice_bound_tvars xs ##>> nice_type ty ##>> nice_name cl
#>> (fn ((xs, ty), cl) => Class_Memb (ident, xs, ty, cl))