--- a/src/HOL/Tools/datatype_rep_proofs.ML Tue Sep 02 14:10:45 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Tue Sep 02 16:55:33 2008 +0200
@@ -187,7 +187,7 @@
alt_name = Name.binding big_rec_name, coind = false, no_elim = true, no_ind = false,
skip_mono = true}
(map (fn s => ((Name.binding s, UnivT'), NoSyn)) rep_set_names') []
- (map (fn x => ((Name.no_binding, []), x)) intr_ts) [] thy1;
+ (map (fn x => (Attrib.no_binding, x)) intr_ts) [] thy1;
(********************************* typedef ********************************)