src/Pure/Isar/local_defs.ML
changeset 21801 c77bc21b3eef
parent 21708 45e7491bea47
child 21844 e10b8bd7a886
     1.1 --- a/src/Pure/Isar/local_defs.ML	Tue Dec 12 20:49:27 2006 +0100
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Tue Dec 12 20:49:28 2006 +0100
     1.3 @@ -74,12 +74,7 @@
     1.4    #> Drule.generalize ([], map (head_of_def o Thm.term_of) defs)
     1.5    #> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
     1.6  
     1.7 -fun expand_term defs =
     1.8 -  let
     1.9 -    val eqs = defs |> map (Thm.term_of #> abs_def #> (fn ((x, U), u) => (x, (U, u))));
    1.10 -    fun get_def (Free (x, _)) = AList.lookup (op =) eqs x
    1.11 -      | get_def _ = NONE;
    1.12 -  in Envir.expand_term get_def end;
    1.13 +val expand_term = Envir.expand_term_frees o map (abs_def o Thm.term_of);
    1.14  
    1.15  fun def_export _ defs = (expand defs, expand_term defs);
    1.16