--- 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
--- 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