--- a/src/HOL/Inductive.thy Tue Jul 03 14:48:27 2007 +0200
+++ b/src/HOL/Inductive.thy Tue Jul 03 15:23:11 2007 +0200
@@ -132,24 +132,19 @@
text{* Lambda-abstractions with pattern matching: *}
syntax
- "_fun_syntax":: "cases_syn => 'a => 'b" ("(%_)" 10)
+ "_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(%_)" 10)
syntax (xsymbols)
- "_fun_syntax":: "cases_syn => 'a => 'b" ("(\<lambda>_)" 10)
+ "_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(\<lambda>_)" 10)
-ML{*
-local
-fun fun_tr ctxt [cs] =
- let val ft = DatatypeCase.case_tr DatatypePackage.datatype_of_constr ctxt
- [Bound 0,cs]
- in Abs("", dummyT, ft) end;
-in
-val trfun_setup =
- Theory.add_advanced_trfuns ([],
- [("_fun_syntax", fun_tr)],
- [], []);
-end
+parse_translation (advanced) {*
+let
+ fun fun_tr ctxt [cs] =
+ let
+ val x = Free (Name.variant (add_term_free_names (cs, [])) "x", dummyT);
+ val ft = DatatypeCase.case_tr DatatypePackage.datatype_of_constr ctxt
+ [x, cs]
+ in lambda x ft end
+in [("_lam_pats_syntax", fun_tr)] end
*}
-setup trfun_setup
-
end