# HG changeset patch
# User wenzelm
# Date 1165952968 -3600
# Node ID c77bc21b3eef776f3aef9fa91cd99f5bc65054ea
# Parent  6035bfcd72d836ecdd73f2cb0be27d3aac29af55
tuned expand_term;

diff -r 6035bfcd72d8 -r c77bc21b3eef src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Tue Dec 12 20:49:27 2006 +0100
+++ b/src/Pure/Isar/local_defs.ML	Tue Dec 12 20:49:28 2006 +0100
@@ -74,12 +74,7 @@
   #> Drule.generalize ([], map (head_of_def o Thm.term_of) defs)
   #> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
 
-fun expand_term defs =
-  let
-    val eqs = defs |> map (Thm.term_of #> abs_def #> (fn ((x, U), u) => (x, (U, u))));
-    fun get_def (Free (x, _)) = AList.lookup (op =) eqs x
-      | get_def _ = NONE;
-  in Envir.expand_term get_def end;
+val expand_term = Envir.expand_term_frees o map (abs_def o Thm.term_of);
 
 fun def_export _ defs = (expand defs, expand_term defs);