src/HOL/Inductive.thy
changeset 23526 936dc616a7fb
parent 23389 aaca6a8e5414
child 23529 958f9d9cfb63
--- a/src/HOL/Inductive.thy	Mon Jul 02 16:42:37 2007 +0200
+++ b/src/HOL/Inductive.thy	Mon Jul 02 23:14:06 2007 +0200
@@ -129,4 +129,27 @@
 
 use "Tools/primrec_package.ML"
 
+text{* Lambda-abstractions with pattern matching: *}
+
+syntax
+  "_fun_syntax":: "cases_syn => 'a => 'b"               ("(%_)" 10)
+syntax (xsymbols)
+  "_fun_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
+*}
+
+setup trfun_setup
+
+end