--- a/src/HOL/datatype.ML Tue Nov 21 14:50:37 1995 +0100
+++ b/src/HOL/datatype.ML Tue Nov 21 14:53:03 1995 +0100
@@ -404,13 +404,13 @@
^ " is not instance of type deduced from equations")
end;
- in
- (thy
- |> add_types types
- |> add_arities arities
- |> add_consts consts
- |> add_trrules xrules
- |> add_axioms rules,add_primrec)
+ in
+ store_datatype (tname, map (fn (x,_,_) => x) cons_list');
+ (thy |> add_types types
+ |> add_arities arities
+ |> add_consts consts
+ |> add_trrules xrules
+ |> add_axioms rules, add_primrec)
end
end
end