changeset 49835 | 31f32ec4d766 |
parent 49833 | 1d80798e8d8a |
child 51551 | 88d1d19fb74f |
--- a/src/HOL/Tools/Datatype/datatype.ML Fri Oct 12 18:58:20 2012 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Fri Oct 12 21:22:35 2012 +0200 @@ -190,7 +190,7 @@ |> Sign.parent_path |> fold_map (fn (((name, mx), tvs), c) => - Typedef.add_typedef_global NONE (name, tvs, mx) + Typedef.add_typedef_global (name, tvs, mx) (Collect $ Const (c, UnivT')) NONE (rtac exI 1 THEN rtac CollectI 1 THEN QUIET_BREADTH_FIRST (has_fewer_prems 1)