src/HOL/Datatype.thy
changeset 33963 977b94b64905
parent 33959 2afc55e8ed27
child 33968 f94fb13ecbb3
     1.1 --- a/src/HOL/Datatype.thy	Fri Nov 27 08:41:08 2009 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Fri Nov 27 08:41:10 2009 +0100
     1.3 @@ -11,6 +11,7 @@
     1.4  imports Product_Type Sum_Type Nat
     1.5  uses
     1.6    ("Tools/Datatype/datatype_rep_proofs.ML")
     1.7 +  ("Tools/Datatype/datatype.ML")
     1.8    ("Tools/inductive_realizer.ML")
     1.9    ("Tools/Datatype/datatype_realizer.ML")
    1.10  begin
    1.11 @@ -520,6 +521,7 @@
    1.12  hide (open) const Push Node Atom Leaf Numb Lim Split Case
    1.13  
    1.14  use "Tools/Datatype/datatype_rep_proofs.ML"
    1.15 +use "Tools/Datatype/datatype.ML"
    1.16  
    1.17  use "Tools/inductive_realizer.ML"
    1.18  setup InductiveRealizer.setup