src/HOL/Inductive.thy
changeset 35115 446c5063e4fd
parent 33968 f94fb13ecbb3
child 37390 8781d80026fc
     1.1 --- a/src/HOL/Inductive.thy	Thu Feb 11 22:55:16 2010 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Thu Feb 11 23:00:22 2010 +0100
     1.3 @@ -301,10 +301,9 @@
     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 = Datatype_Case.case_tr true Datatype_Data.info_of_constr
     1.8 -                 ctxt [x, cs]
     1.9 +      val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr ctxt [x, cs];
    1.10      in lambda x ft end
    1.11 -in [("_lam_pats_syntax", fun_tr)] end
    1.12 +in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
    1.13  *}
    1.14  
    1.15  end