# HG changeset patch
# User wenzelm
# Date 1164239531 -3600
# Node ID e2cc70e70b2f131f4f373f82f2662be569cdf42e
# Parent  63e7eb863ae61d4bdd604d1b52148eff76189cbd
replaced map_values by morph_values;

diff -r 63e7eb863ae6 -r e2cc70e70b2f src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Thu Nov 23 00:52:07 2006 +0100
+++ b/src/Pure/Isar/args.ML	Thu Nov 23 00:52:11 2006 +0100
@@ -28,8 +28,7 @@
   val dest_src: src -> (string * T list) * Position.T
   val pretty_src: Proof.context -> src -> Pretty.T
   val map_name: (string -> string) -> src -> src
-  val map_values: (string -> string) -> (typ -> typ) -> (term -> term) -> (thm -> thm)
-    -> src -> src
+  val morph_values: morphism -> src -> src
   val maxidx_values: src -> int -> int
   val assignable: src -> src
   val assign: value option -> T -> unit
@@ -181,11 +180,11 @@
 fun map_value f (Arg (s, Value (SOME v))) = Arg (s, Value (SOME (f v)))
   | map_value _ arg = arg;
 
-fun map_values f g h i = map_args (map_value
-  (fn Name s => Name (f s)
-    | Typ T => Typ (g T)
-    | Term t => Term (h t)
-    | Fact ths => Fact (map i ths)
+fun morph_values phi = map_args (map_value
+  (fn Name s => Name (Morphism.name phi s)
+    | Typ T => Typ (Morphism.typ phi T)
+    | Term t => Term (Morphism.term phi t)
+    | Fact ths => Fact (map (Morphism.thm phi) ths)
     | Attribute att => Attribute att));
 
 fun maxidx_values (Src ((_, args), _)) = args |> fold