src/HOL/Inductive.thy
changeset 51678 1e33b81c328a
parent 51674 2b1498a2ce85
child 51679 e7316560928b
     1.1 --- a/src/HOL/Inductive.thy	Fri Apr 05 22:08:42 2013 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Fri Apr 05 22:08:42 2013 +0200
     1.3 @@ -275,7 +275,7 @@
     1.4  ML_file "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup
     1.5  
     1.6  consts
     1.7 -  case_guard :: "'a \<Rightarrow> 'a"
     1.8 +  case_guard :: "bool \<Rightarrow> 'a \<Rightarrow> 'a"
     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 @@ -299,7 +299,7 @@
    1.13    fun fun_tr ctxt [cs] =
    1.14      let
    1.15        val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
    1.16 -      val ft = Case_Translation.case_tr ctxt [x, cs];
    1.17 +      val ft = Case_Translation.case_tr true ctxt [x, cs];
    1.18      in lambda x ft end
    1.19  in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
    1.20  *}