moved lambda to Pure/term.ML;
authorwenzelm
Wed, 24 Oct 2001 17:38:29 +0200
changeset 11923 929d97ed8c0f
parent 11922 78857e6107cb
child 11924 b6def266cbb9
moved lambda to Pure/term.ML;
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);