author wenzelm Wed, 14 Nov 2001 23:18:13 +0100 changeset 12187 a1000fcf636e parent 12186 9b7026a0b0ed child 12188 e4279b7fb8cc
use proper intr_names (for required case_names); store con_defs, case_eqns, recursor_eqns, free_iffs, free_elims;
```--- a/src/ZF/Tools/datatype_package.ML	Wed Nov 14 23:16:05 2001 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Wed Nov 14 23:18:13 2001 +0100
@@ -243,12 +243,11 @@
|>> Theory.parent_path

+  val intr_names = map #2 (flat con_ty_lists);
val (thy1, ind_result) =
-                    false (rec_tms, dom_sum) (map (fn tm => (("", tm), [])) intr_tms)
-                           (monos, con_defs,
-                           type_intrs @ Datatype_Arg.intrs,
-                           type_elims @ Datatype_Arg.elims)
+      false (rec_tms, dom_sum) (map Thm.no_attributes (intr_names ~~ intr_tms))
+      (monos, con_defs, type_intrs @ Datatype_Arg.intrs, type_elims @ Datatype_Arg.elims);

(**** Now prove the datatype theorems in this theory ****)

@@ -282,7 +281,7 @@
(cterm_of (sign_of thy1) (mk_case_eqn arg)))
(case_tacsf con_def);

-  val free_iffs = con_defs RL [Ind_Syntax.def_swap_iff];
+  val free_iffs = map standard (con_defs RL [Ind_Syntax.def_swap_iff]);

val case_eqns =
map prove_case_eqn
@@ -333,7 +332,7 @@
val constructors =
map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs);

-  val free_SEs = Ind_Syntax.mk_free_SEs free_iffs;
+  val free_SEs = map standard (Ind_Syntax.mk_free_SEs free_iffs);

val {intrs, elim, induct, mutual_induct, ...} = ind_result

@@ -372,7 +371,12 @@