Corrected display of split f t: no more let.
Also replaced "_abs" by "_lambda" --- the former was a mistake which
happended to work.

--- 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