src/HOL/Inductive.thy
changeset 45891 d73605c829cc
parent 45890 5f70aaecae26
child 45897 65cef0298158
     1.1 --- a/src/HOL/Inductive.thy	Thu Dec 15 17:37:14 2011 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Thu Dec 15 18:08:40 2011 +0100
     1.3 @@ -11,9 +11,9 @@
     1.4    "Tools/dseq.ML"
     1.5    "Tools/Datatype/datatype_aux.ML"
     1.6    "Tools/Datatype/datatype_prop.ML"
     1.7 -  "Tools/Datatype/datatype_case.ML"
     1.8    ("Tools/Datatype/datatype_abs_proofs.ML")
     1.9    ("Tools/Datatype/datatype_data.ML")
    1.10 +  ("Tools/Datatype/datatype_case.ML")
    1.11    ("Tools/Datatype/rep_datatype.ML")
    1.12    ("Tools/primrec.ML")
    1.13    ("Tools/Datatype/datatype_codegen.ML")
    1.14 @@ -277,9 +277,8 @@
    1.15  text {* Package setup. *}
    1.16  
    1.17  use "Tools/Datatype/datatype_abs_proofs.ML"
    1.18 -use "Tools/Datatype/datatype_data.ML"
    1.19 -setup Datatype_Data.setup
    1.20 -
    1.21 +use "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup
    1.22 +use "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup
    1.23  use "Tools/Datatype/rep_datatype.ML"
    1.24  
    1.25  use "Tools/Datatype/datatype_codegen.ML"
    1.26 @@ -300,7 +299,7 @@
    1.27      let
    1.28        (* FIXME proper name context!? *)
    1.29        val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT);
    1.30 -      val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr_permissive ctxt [x, cs];
    1.31 +      val ft = Datatype_Case.case_tr true ctxt [x, cs];
    1.32      in lambda x ft end
    1.33  in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
    1.34  *}