--- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Oct 18 21:01:18 2001 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Oct 18 21:01:59 2001 +0200
@@ -181,8 +181,9 @@
val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
setmp TypedefPackage.quiet_mode true
- (TypedefPackage.add_typedef_i false name' (name, tvs, mx) c None
- (QUIET_BREADTH_FIRST (has_fewer_prems 1)
+ (TypedefPackage.add_typedef_i false (Some name') (name, tvs, mx) c None
+ (rtac exI 1 THEN
+ QUIET_BREADTH_FIRST (has_fewer_prems 1)
(resolve_tac (Funs_nonempty::rep_intrs) 1))) thy |> #1)
(parent_path flat_names thy2, types_syntax ~~ tyvars ~~
(take (length newTs, consts)) ~~ new_type_names));