src/HOL/Inductive.thy
changeset 51673 4dfa00e264d8
parent 51672 d5c5e088ebdf
child 51674 2b1498a2ce85
     1.1 --- a/src/HOL/Inductive.thy	Tue Jan 22 13:32:41 2013 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Tue Jan 22 14:33:45 2013 +0100
     1.3 @@ -279,7 +279,8 @@
     1.4    case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
     1.5    case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
     1.6    case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b"
     1.7 -ML_file "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup
     1.8 +ML_file "Tools/case_translation.ML"
     1.9 +setup Case_Translation.setup
    1.10  
    1.11  ML_file "Tools/Datatype/rep_datatype.ML"
    1.12  ML_file "Tools/Datatype/datatype_codegen.ML" setup Datatype_Codegen.setup
    1.13 @@ -297,7 +298,7 @@
    1.14    fun fun_tr ctxt [cs] =
    1.15      let
    1.16        val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
    1.17 -      val ft = Datatype_Case.case_tr ctxt [x, cs];
    1.18 +      val ft = Case_Translation.case_tr ctxt [x, cs];
    1.19      in lambda x ft end
    1.20  in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
    1.21  *}