# HG changeset patch
# User nipkow
# Date 799482113 -7200
# Node ID 884c6ef06fbfd720a44bfd581bfb2d91dd613349
# Parent  13c35eb5169ba6d2ab079474d74f5faa248203b8
Corrected display of split f t: no more let.
Also replaced "_abs" by "_lambda" --- the former was a mistake which
happended to work.

diff -r 13c35eb5169b -r 884c6ef06fbf src/HOL/Prod.thy
--- a/src/HOL/Prod.thy	Tue May 02 19:59:06 1995 +0200
+++ b/src/HOL/Prod.thy	Wed May 03 08:21:53 1995 +0200
@@ -95,11 +95,7 @@
 
 fun split_tr'(t::args) =
   let val (pats,ft) = split2(t)
-  in case args of
-       [] => const"_abs" $ pttrn pats $ ft
-     | arg::rest =>
-         list_comb(const"_Let"$(const"_bind"$(pttrn pats)$arg)$ft, rest)
-  end
+  in list_comb(const"_lambda" $ pttrn pats $ ft, args) end;
 
 in