src/HOL/Inductive.thy
changeset 33963 977b94b64905
parent 33959 2afc55e8ed27
child 33966 b863967f23ea
     1.1 --- a/src/HOL/Inductive.thy	Fri Nov 27 08:41:08 2009 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Fri Nov 27 08:41:10 2009 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4    "Tools/Datatype/datatype_prop.ML"
     1.5    "Tools/Datatype/datatype_case.ML"
     1.6    ("Tools/Datatype/datatype_abs_proofs.ML")
     1.7 -  ("Tools/Datatype/datatype.ML")
     1.8 +  ("Tools/Datatype/datatype_data.ML")
     1.9    ("Tools/old_primrec.ML")
    1.10    ("Tools/primrec.ML")
    1.11    ("Tools/Datatype/datatype_codegen.ML")
    1.12 @@ -282,8 +282,8 @@
    1.13  text {* Package setup. *}
    1.14  
    1.15  use "Tools/Datatype/datatype_abs_proofs.ML"
    1.16 -use "Tools/Datatype/datatype.ML"
    1.17 -setup Datatype.setup
    1.18 +use "Tools/Datatype/datatype_data.ML"
    1.19 +setup Datatype_Data.setup
    1.20  
    1.21  use "Tools/old_primrec.ML"
    1.22  use "Tools/primrec.ML"
    1.23 @@ -306,7 +306,7 @@
    1.24    fun fun_tr ctxt [cs] =
    1.25      let
    1.26        val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
    1.27 -      val ft = DatatypeCase.case_tr true Datatype.info_of_constr
    1.28 +      val ft = DatatypeCase.case_tr true Datatype_Data.info_of_constr
    1.29                   ctxt [x, cs]
    1.30      in lambda x ft end
    1.31  in [("_lam_pats_syntax", fun_tr)] end