# HG changeset patch
# User wenzelm
# Date 1128718764 -7200
# Node ID f06d6498ebf0eb761d2a20302a3230157a75be79
# Parent  8d928051d6a7d8f02d14b4740bd0e8f7671c7ce9
added absdummy;

diff -r 8d928051d6a7 -r f06d6498ebf0 src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Oct 07 22:59:23 2005 +0200
+++ b/src/Pure/term.ML	Fri Oct 07 22:59:24 2005 +0200
@@ -112,6 +112,7 @@
   val abstract_over: term * term -> term
   val lambda: term -> term -> term
   val absfree: string * typ * term -> term
+  val absdummy: typ * term -> term
   val list_abs_free: (string * typ) list * term -> term
   val list_all_free: (string * typ) list * term -> term
   val list_all: (string * typ) list * term -> term
@@ -894,6 +895,7 @@
 
 (*Form an abstraction over a free variable.*)
 fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));
+fun absdummy (T, body) = Abs ("uu", T, body);
 
 (*Abstraction over a list of free variables*)
 fun list_abs_free ([ ] ,     t) = t