reintroduced syntax for "nonexhaustive" datatypes

--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu May 16 13:05:52 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu May 16 13:05:52 2013 +0200
@@ -51,7 +51,7 @@
     Type_Decl of string * 'a * int |
     Sym_Decl of string * 'a * 'a ho_type |
     Datatype_Decl of string * ('a * 'a list) list * 'a ho_type
-                     * ('a, 'a ho_type) ho_term list |
+                     * ('a, 'a ho_type) ho_term list * bool |
     Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a |
     Formula of (string * string) * formula_role
                * ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula
@@ -194,7 +194,7 @@
   Type_Decl of string * 'a * int |
   Sym_Decl of string * 'a * 'a ho_type |
   Datatype_Decl of string * ('a * 'a list) list * 'a ho_type
-                   * ('a, 'a ho_type) ho_term list |
+                   * ('a, 'a ho_type) ho_term list * bool |
   Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a |
   Formula of (string * string) * formula_role
              * ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula
@@ -601,8 +601,9 @@
       (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 =
-      "datatype(" ^ commas (binder_typ xs ty :: map term tms) ^ ")."
+    fun datatype_decl xs ty tms exhaust =
+      "datatype(" ^ commas (binder_typ xs ty :: map term tms @
+                            (if exhaust then [] else ["..."])) ^ ")."
     fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")."
     fun formula pred (Formula ((ident, alt), kind, phi, _, info)) =
         if pred kind then
@@ -650,8 +651,8 @@
                else NONE
              | _ => NONE) |> flat
     val datatype_decls =
-      filt (try (fn Datatype_Decl (_, xs, ty, tms) => datatype_decl xs ty tms))
-      |> flat
+      filt (try (fn Datatype_Decl (_, xs, ty, tms, exhaust) =>
+                    datatype_decl xs ty tms exhaust)) |> flat
     val sort_decls =
       filt (try (fn Class_Memb (_, xs, ty, cl) => sort_decl xs ty cl)) |> flat
     val subclass_decls =
@@ -929,9 +930,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)) =
+      | nice_line (Datatype_Decl (ident, xs, ty, tms, exhaust)) =
         nice_bound_tvars xs ##>> nice_type ty ##>> fold_map nice_term tms
-        #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms))
+        #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms, exhaust))
       | 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))

--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu May 16 13:05:52 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu May 16 13:05:52 2013 +0200
@@ -2546,20 +2546,21 @@
     in
       if is_type_enc_polymorphic type_enc then
         [(native_ho_type_from_typ type_enc false 0 @{typ nat},
-          map ho_term_from_term [@{term "0::nat"}, @{term Suc}]),
+          map ho_term_from_term [@{term "0::nat"}, @{term Suc}], true),
          (native_ho_type_from_typ type_enc false 0 (Logic.varifyT_global @{typ "'a list"}),
-          map (ho_term_from_term o Logic.varify_types_global) [@{term Nil}, @{term Cons}])]
+          map (ho_term_from_term o Logic.varify_types_global) [@{term Nil}, @{term Cons}],
+          true)]
       else
         []
     end
   | datatypes_of_sym_table _ _ _ _ _ = []
 
-fun decl_line_of_datatype (ty as AType ((_, s'), ty_args), ctrs) =
+fun decl_line_of_datatype (ty as AType ((_, s'), ty_args), ctrs, exhaust) =
   let
     val xs = map (fn AType (name, []) => name) ty_args
   in
     Datatype_Decl (datatype_decl_prefix ^ ascii_of s', map (rpair []) xs, ty,
-                   ctrs)
+                   ctrs, exhaust)
   end
 
 fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
@@ -2679,7 +2680,7 @@
     fun do_line (Class_Decl (_, _, cls)) = fold do_class cls
       | do_line (Type_Decl _) = I
       | do_line (Sym_Decl (_, _, ty)) = do_type ty
-      | do_line (Datatype_Decl (_, xs, ty, tms)) =
+      | do_line (Datatype_Decl (_, xs, ty, tms, _)) =
         fold do_bound_tvars xs #> do_type ty #> fold (do_term false) tms
       | do_line (Class_Memb (_, xs, ty, cl)) =
         fold do_bound_tvars xs #> do_type ty #> do_class cl