--- a/src/HOL/Inductive.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Inductive.thy Sat May 25 15:37:53 2013 +0200
@@ -299,14 +299,14 @@
syntax (xsymbols)
"_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(\<lambda>_)" 10)
-parse_translation (advanced) {*
-let
- fun fun_tr ctxt [cs] =
- let
- val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
- val ft = Case_Translation.case_tr true ctxt [x, cs];
- in lambda x ft end
-in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
+parse_translation {*
+ let
+ fun fun_tr ctxt [cs] =
+ let
+ val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
+ val ft = Case_Translation.case_tr true ctxt [x, cs];
+ in lambda x ft end
+ in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
*}
end