merged
authorwenzelm
Wed, 27 Apr 2011 23:04:28 +0200
changeset 42498 9e1a77ad7ca3
parent 42497 89acb654d8eb (diff)
parent 42496 65ec88b369fd (current diff)
child 42500 b99cc6f7df63
merged
src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Wed Apr 27 23:02:43 2011 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -17,7 +17,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
@@ -64,11 +63,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 23:02:43 2011 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Wed Apr 27 23:04:28 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