# HG changeset patch
# User wenzelm
# Date 1003937909 -7200
# Node ID 929d97ed8c0ff95c8497b6ddd9654ad887304e69
# Parent  78857e6107cb813aaa06445d7cfababfc17630c5
moved lambda to Pure/term.ML;

diff -r 78857e6107cb -r 929d97ed8c0f src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Oct 24 17:38:19 2001 +0200
+++ b/src/HOL/Tools/record_package.ML	Wed Oct 24 17:38:29 2001 +0200
@@ -69,10 +69,6 @@
 val (op :==) = Logic.mk_defpair;
 val (op ===) = HOLogic.mk_Trueprop o HOLogic.mk_eq;
 
-fun lambda v t =
-  let val (x, T) = Term.dest_Free v
-  in Abs (x, T, abstract_over (v, t)) end;
-
 fun prefix_base s = NameSpace.map_base (fn bname => s ^ bname);