--- a/src/HOL/Tools/datatype_rep_proofs.ML Fri Sep 28 10:30:51 2007 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Fri Sep 28 10:32:38 2007 +0200
@@ -178,7 +178,7 @@
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
setmp InductivePackage.quiet_mode (! quiet_mode)
(InductivePackage.add_inductive_global false big_rec_name false true false
- (map (fn s => (s, SOME UnivT', NoSyn)) rep_set_names') []
+ (map (fn s => ((s, UnivT'), NoSyn)) rep_set_names') []
(map (fn x => (("", []), x)) intr_ts) []) thy1;
(********************************* typedef ********************************)