# HG changeset patch
# User wenzelm
# Date 1220357419 -7200
# Node ID 90adbbf0318798e53dcd1f8c956d42687bafebdf
# Parent  5e9f00f4f209ab8897b094bf053b1629323bf457
name/var morphism operates on Name.binding;

diff -r 5e9f00f4f209 -r 90adbbf03187 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Tue Sep 02 12:07:34 2008 +0200
+++ b/src/Pure/morphism.ML	Tue Sep 02 14:10:19 2008 +0200
@@ -17,21 +17,21 @@
 signature MORPHISM =
 sig
   include BASIC_MORPHISM
-  val var: morphism -> string * mixfix -> string * mixfix
-  val name: morphism -> string -> string
+  val var: morphism -> Name.binding * mixfix -> Name.binding * mixfix
+  val name: morphism -> Name.binding -> Name.binding
   val typ: morphism -> typ -> typ
   val term: morphism -> term -> term
   val fact: morphism -> thm list -> thm list
   val thm: morphism -> thm -> thm
   val cterm: morphism -> cterm -> cterm
   val morphism:
-   {name: string -> string,
-    var: string * mixfix -> string * mixfix,
+   {name: Name.binding -> Name.binding,
+    var: Name.binding * mixfix -> Name.binding * mixfix,
     typ: typ -> typ,
     term: term -> term,
     fact: thm list -> thm list} -> morphism
-  val name_morphism: (string -> string) -> morphism
-  val var_morphism: (string * mixfix -> string * mixfix) -> morphism
+  val name_morphism: (Name.binding -> Name.binding) -> morphism
+  val var_morphism: (Name.binding * mixfix -> Name.binding * mixfix) -> morphism
   val typ_morphism: (typ -> typ) -> morphism
   val term_morphism: (term -> term) -> morphism
   val fact_morphism: (thm list -> thm list) -> morphism
@@ -46,8 +46,8 @@
 struct
 
 datatype morphism = Morphism of
- {name: string -> string,
-  var: string * mixfix -> string * mixfix,
+ {name: Name.binding -> Name.binding,
+  var: Name.binding * mixfix -> Name.binding * mixfix,
   typ: typ -> typ,
   term: term -> term,
   fact: thm list -> thm list};
diff -r 5e9f00f4f209 -r 90adbbf03187 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Tue Sep 02 12:07:34 2008 +0200
+++ b/src/Pure/simplifier.ML	Tue Sep 02 14:10:19 2008 +0200
@@ -194,7 +194,7 @@
   in
     lthy |> LocalTheory.declaration (fn phi =>
       let
-        val name' = Morphism.name phi name;
+        val name' = Name.name_of (Morphism.name phi (Name.binding name));
         val simproc' = morph_simproc phi simproc;
       in
         Simprocs.map (fn simprocs =>