# HG changeset patch
# User wenzelm
# Date 1165510725 -3600
# Node ID 6c07cc87fe2b8e39a34a9d2c0c42527761f89dcd
# Parent  9f65fecb6e10429be8ce8a3fe3b00b13010cd7a6
added expand_term;

diff -r 9f65fecb6e10 -r 6c07cc87fe2b src/Pure/envir.ML
--- a/src/Pure/envir.ML	Thu Dec 07 17:58:44 2006 +0100
+++ b/src/Pure/envir.ML	Thu Dec 07 17:58:45 2006 +0100
@@ -39,6 +39,7 @@
   val subst_Vars: tenv -> term -> term
   val subst_vars: Type.tyenv * tenv -> term -> term
   val expand_atom: typ -> typ * term -> term
+  val expand_term: (term -> (typ * term) option) -> term -> term
 end;
 
 structure Envir : ENVIR =
@@ -295,10 +296,28 @@
   in subst end;
 
 
-(* expand_atom *)
+(* expand defined atoms *)
 
 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 =
+  let
+    fun expand tm =
+      let
+        val (head, args) = Term.strip_comb tm;
+        val args' = map expand args;
+        fun comb head' = Term.list_comb (head', args');
+      in
+        (case head of
+          Abs (x, T, t) => comb (Abs (x, T, expand t))
+        | _ =>
+            (case get_def head of
+              SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args')
+            | NONE => comb head)
+        | _ => comb head)
+      end;
+  in expand end;
+
 end;