# HG changeset patch
# User krauss
# Date 1303931867 -7200
# Node ID 89acb654d8eb2298d8193af9d3ce766f76dff8eb
# Parent  2777a27506d0d8a56f5df615e82e240e1be04ea9
inlined Function_Lib.replace_frees, which is used only once

diff -r 2777a27506d0 -r 89acb654d8eb src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Wed Apr 27 13:21:12 2011 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML	Wed Apr 27 21:17:47 2011 +0200
@@ -18,7 +18,6 @@
 
   val unordered_pairs: 'a list -> ('a * 'a) list
 
-  val replace_frees: (string * term) list -> term -> term
   val rename_bound: string -> term -> term
   val mk_forall_rename: (string * term) -> term -> term
   val forall_intr_rename: (string * cterm) -> thm -> thm
@@ -78,11 +77,7 @@
   | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs
 
 
-(* Replaces Frees by name. Works with loose Bounds. *)
-fun replace_frees assoc =
-  map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n)
-    | t => t)
-
+(* renaming bound variables *)
 
 fun rename_bound n (Q $ Abs (_, T, b)) = (Q $ Abs (n, T, b))
   | rename_bound n _ = raise Match
diff -r 2777a27506d0 -r 89acb654d8eb src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Wed Apr 27 13:21:12 2011 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Wed Apr 27 21:17:47 2011 +0200
@@ -114,10 +114,11 @@
     fun convert_eqs (f, qs, gs, args, rhs) =
       let
         val MutualPart {i, i', ...} = get_part f parts
+        val rhs' = rhs
+          |> map_aterms (fn t as Free (n, _) => the_default t (AList.lookup (op =) rews n) | t => t)
       in
         (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args),
-         SumTree.mk_inj RST n' i' (replace_frees rews rhs)
-         |> Envir.beta_norm)
+         Envir.beta_norm (SumTree.mk_inj RST n' i' rhs'))
       end
 
     val qglrs = map convert_eqs fqgars