src/HOL/Inductive.thy
changeset 51672 d5c5e088ebdf
parent 50302 9149a07a6c67
child 51673 4dfa00e264d8
     1.1 --- a/src/HOL/Inductive.thy	Wed Apr 10 13:10:38 2013 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Tue Jan 22 13:32:41 2013 +0100
     1.3 @@ -273,7 +273,14 @@
     1.4  ML_file "Tools/Datatype/datatype_aux.ML"
     1.5  ML_file "Tools/Datatype/datatype_prop.ML"
     1.6  ML_file "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup
     1.7 +
     1.8 +consts
     1.9 +  case_nil :: "'a \<Rightarrow> 'b"
    1.10 +  case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.11 +  case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
    1.12 +  case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b"
    1.13  ML_file "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup
    1.14 +
    1.15  ML_file "Tools/Datatype/rep_datatype.ML"
    1.16  ML_file "Tools/Datatype/datatype_codegen.ML" setup Datatype_Codegen.setup
    1.17  ML_file "Tools/Datatype/primrec.ML"
    1.18 @@ -290,7 +297,7 @@
    1.19    fun fun_tr ctxt [cs] =
    1.20      let
    1.21        val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
    1.22 -      val ft = Datatype_Case.case_tr true ctxt [x, cs];
    1.23 +      val ft = Datatype_Case.case_tr ctxt [x, cs];
    1.24      in lambda x ft end
    1.25  in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
    1.26  *}