src/HOL/Datatype.thy
changeset 33963 977b94b64905
parent 33959 2afc55e8ed27
child 33968 f94fb13ecbb3
--- a/src/HOL/Datatype.thy	Fri Nov 27 08:41:08 2009 +0100
+++ b/src/HOL/Datatype.thy	Fri Nov 27 08:41:10 2009 +0100
@@ -11,6 +11,7 @@
 imports Product_Type Sum_Type Nat
 uses
   ("Tools/Datatype/datatype_rep_proofs.ML")
+  ("Tools/Datatype/datatype.ML")
   ("Tools/inductive_realizer.ML")
   ("Tools/Datatype/datatype_realizer.ML")
 begin
@@ -520,6 +521,7 @@
 hide (open) const Push Node Atom Leaf Numb Lim Split Case
 
 use "Tools/Datatype/datatype_rep_proofs.ML"
+use "Tools/Datatype/datatype.ML"
 
 use "Tools/inductive_realizer.ML"
 setup InductiveRealizer.setup