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