src/HOL/Inductive.thy
changeset 52143 36ffe23b25f8
parent 51692 ecd34f863242
child 54398 100c0eaf63d5
     1.1 --- a/src/HOL/Inductive.thy	Sat May 25 15:00:53 2013 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Sat May 25 15:37:53 2013 +0200
     1.3 @@ -299,14 +299,14 @@
     1.4  syntax (xsymbols)
     1.5    "_lam_pats_syntax" :: "cases_syn => 'a => 'b"               ("(\<lambda>_)" 10)
     1.6  
     1.7 -parse_translation (advanced) {*
     1.8 -let
     1.9 -  fun fun_tr ctxt [cs] =
    1.10 -    let
    1.11 -      val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
    1.12 -      val ft = Case_Translation.case_tr true ctxt [x, cs];
    1.13 -    in lambda x ft end
    1.14 -in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
    1.15 +parse_translation {*
    1.16 +  let
    1.17 +    fun fun_tr ctxt [cs] =
    1.18 +      let
    1.19 +        val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
    1.20 +        val ft = Case_Translation.case_tr true ctxt [x, cs];
    1.21 +      in lambda x ft end
    1.22 +  in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
    1.23  *}
    1.24  
    1.25  end