src/HOL/Inductive.thy
changeset 31784 bd3486c57ba3
parent 31775 2b04504fcb69
child 31949 3f933687fae9
     1.1 --- a/src/HOL/Inductive.thy	Tue Jun 23 15:32:34 2009 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Tue Jun 23 16:27:12 2009 +0200
     1.3 @@ -364,7 +364,7 @@
     1.4    fun fun_tr ctxt [cs] =
     1.5      let
     1.6        val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
     1.7 -      val ft = DatatypeCase.case_tr true Datatype.datatype_of_constr
     1.8 +      val ft = DatatypeCase.case_tr true Datatype.info_of_constr
     1.9                   ctxt [x, cs]
    1.10      in lambda x ft end
    1.11  in [("_lam_pats_syntax", fun_tr)] end