# HG changeset patch
# User clasohm
# Date 816961983 -3600
# Node ID 6bdee79ef125d668f74a4bc137dc1792edb12bee
# Parent  71124bd19b40f64f74527fb56d0bc4e80b344f8c
added call of store_datatype

diff -r 71124bd19b40 -r 6bdee79ef125 src/HOL/datatype.ML
--- 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