# HG changeset patch
# User berghofe
# Date 1035213259 -7200
# Node ID 66e151df01c80c906e396de10b97c60c3921e791
# Parent  cfe1dc32c2e56c73d5154e7fd6fb74ecce1fc0a4
- removed flexpair
- added maxidx_of_terms
- tuned lambda: now also abstracts over Vars

diff -r cfe1dc32c2e5 -r 66e151df01c8 src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Oct 21 17:12:44 2002 +0200
+++ b/src/Pure/term.ML	Mon Oct 21 17:14:19 2002 +0200
@@ -83,7 +83,6 @@
   val implies: term
   val all: typ -> term
   val equals: typ -> term
-  val flexpair: typ -> term
   val strip_all_body: term -> term
   val strip_all_vars: term -> (string * typ) list
   val incr_bv: int * int * term -> term
@@ -135,6 +134,7 @@
   val maxidx_of_typ: typ -> int
   val maxidx_of_typs: typ list -> int
   val maxidx_of_term: term -> int
+  val maxidx_of_terms: term list -> int
   val read_radixint: int * string list -> int * string list
   val read_int: string list -> int * string list
   val oct_char: string -> string
@@ -434,8 +434,6 @@
 
 fun equals T = Const("==", T-->T-->propT);
 
-fun flexpair T = Const("=?=", T-->T-->propT);
-
 (* maps  !!x1...xn. t   to   t  *)
 fun strip_all_body (Const("all",_)$Abs(_,_,t))  =  strip_all_body t
   | strip_all_body t  =  t;
@@ -648,9 +646,9 @@
         | _ => u)
   in  abst(0,body)  end;
 
-fun lambda v t =
-  let val (x, T) = dest_Free v
-  in Abs (x, T, abstract_over (v, t)) end;
+fun lambda (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t))
+  | lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
+  | lambda v t = raise TERM ("lambda", [v, t]);
 
 (*Form an abstraction over a free variable.*)
 fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));
@@ -726,6 +724,8 @@
   | maxidx_of_term (Abs (_,T,u)) = Int.max(maxidx_of_term u, maxidx_of_typ T)
   | maxidx_of_term (f$t) = Int.max(maxidx_of_term f,  maxidx_of_term t);
 
+fun maxidx_of_terms ts = foldl Int.max (~1, map maxidx_of_term ts);
+
 
 (* Increment the index of all Poly's in T by k *)
 fun incr_tvar k = map_type_tvar (fn ((a,i),S) => TVar((a,i+k),S));