--- a/src/HOL/Tools/datatype_package.ML Tue Jan 12 16:00:31 1999 +0100
+++ b/src/HOL/Tools/datatype_package.ML Tue Jan 12 16:42:21 1999 +0100
@@ -31,18 +31,7 @@
induction : thm,
size : thm list,
simps : thm list}
- val rep_datatype : string list option -> xstring list list ->
- xstring list list -> xstring -> theory -> theory *
- {distinct : thm list list,
- inject : thm list list,
- exhaustion : thm list,
- rec_thms : thm list,
- case_thms : thm list list,
- split_thms : (thm * thm) list,
- induction : thm,
- size : thm list,
- simps : thm list}
- val rep_datatype_i : string list option -> thm list list ->
+ val rep_datatype : string list option -> thm list list ->
thm list list -> thm -> theory -> theory *
{distinct : thm list list,
inject : thm list list,
@@ -483,14 +472,10 @@
(*********************** declare non-datatype as datatype *********************)
-fun gen_rep_datatype get get' alt_names distinct_names inject_names induction_name thy =
+fun rep_datatype alt_names distinct inject induction thy =
let
val sign = sign_of thy;
- val distinct = map (get thy) distinct_names;
- val inject = map (get thy) inject_names;
- val induction = get' thy induction_name;
-
val induction' = freezeT induction;
fun err t = error ("Ill-formed predicate in induction rule: " ^
@@ -571,8 +556,6 @@
simps = simps})
end;
-val rep_datatype = gen_rep_datatype (fn thy => PureThy.get_thmss thy) get_thm;
-val rep_datatype_i = gen_rep_datatype (K I) (K I);
(******************************** add datatype ********************************)
--- a/src/HOL/thy_syntax.ML Tue Jan 12 16:00:31 1999 +0100
+++ b/src/HOL/thy_syntax.ML Tue Jan 12 16:42:21 1999 +0100
@@ -134,22 +134,25 @@
";\nlocal\n\
\val (thy, {distinct, inject, exhaustion, rec_thms,\n\
\ case_thms, split_thms, induction, size, simps}) =\n\
- \ DatatypePackage.add_datatype false " ^ add_datatype_args ^ " thy;\n\
+ \ DatatypePackage.add_datatype false " ^ add_datatype_args ^ " thy;\n\
\in\n" ^ mk_bind_thms_string names ^
"val thy = thy;\nend;\nval thy = thy\n"
end;
+ fun mk_thmss namess = "(map (PureThy.get_thmss thy) " ^ mk_list (map mk_list namess) ^ ")";
+ fun mk_thm name = "(PureThy.get_thm thy " ^ name ^ ")";
+
fun mk_rep_dt_string (((names, distinct), inject), induct) =
";\nlocal\n\
\val (thy, {distinct, inject, exhaustion, rec_thms,\n\
\ case_thms, split_thms, induction, size, simps}) =\n\
- \ DatatypePackage.rep_datatype " ^
+ \ DatatypePackage.rep_datatype " ^
(case names of
- Some names => "(Some [" ^ commas_quote names ^ "]) " ^
- mk_list (map mk_list distinct) ^ " " ^ mk_list (map mk_list inject) ^
- " " ^ induct ^ " thy;\nin\n" ^ mk_bind_thms_string names
- | None => "None " ^ mk_list (map mk_list distinct) ^ " " ^
- mk_list (map mk_list inject) ^ " " ^ induct ^ " thy;\nin\n") ^
+ Some names => "(Some [" ^ commas_quote names ^ "])\n " ^
+ mk_thmss distinct ^ "\n " ^ mk_thmss inject ^
+ "\n " ^ mk_thm induct ^ " thy;\nin\n" ^ mk_bind_thms_string names
+ | None => "None\n " ^ mk_thmss distinct ^ "\n " ^ mk_thmss inject ^
+ "\n " ^ mk_thm induct ^ " thy;\nin\n") ^
"val thy = thy;\nend;\nval thy = thy\n";
(*** parsers ***)