# HG changeset patch
# User wenzelm
# Date 1165952962 -3600
# Node ID d7dcc3dfa7e9ceb948d5fec8126df28afb4eb30c
# Parent  1a9f57f1bc3ada39ec3b006aa7ee6f089779c580
added expand_term_frees;

diff -r 1a9f57f1bc3a -r d7dcc3dfa7e9 src/Pure/envir.ML
--- a/src/Pure/envir.ML	Tue Dec 12 20:49:21 2006 +0100
+++ b/src/Pure/envir.ML	Tue Dec 12 20:49:22 2006 +0100
@@ -40,6 +40,7 @@
   val subst_vars: Type.tyenv * tenv -> term -> term
   val expand_atom: typ -> typ * term -> term
   val expand_term: (term -> (typ * term) option) -> term -> term
+  val expand_term_frees: ((string * typ) * term) list -> term -> term
 end;
 
 structure Envir : ENVIR =
@@ -296,13 +297,13 @@
   in subst end;
 
 
-(* expand defined atoms *)
+(* expand defined atoms -- with local beta reduction *)
 
 fun expand_atom T (U, u) =
   subst_TVars (Type.raw_match (U, T) Vartab.empty) u
   handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
 
-fun expand_term get_def =
+fun expand_term get =
   let
     fun expand tm =
       let
@@ -313,11 +314,17 @@
         (case head of
           Abs (x, T, t) => comb (Abs (x, T, expand t))
         | _ =>
-            (case get_def head of
+            (case get head of
               SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args')
             | NONE => comb head)
         | _ => comb head)
       end;
   in expand end;
 
+fun expand_term_frees defs =
+  let
+    val eqs = map (fn ((x, U), u) => (x, (U, u))) defs;
+    val get = fn Free (x, _) => AList.lookup (op =) eqs x | _ => NONE;
+  in expand_term get end;
+
 end;