diff -r f6d9e0e0b153 -r 1de908189869 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Wed Dec 03 21:00:39 2008 -0800
+++ b/src/Pure/morphism.ML	Thu Dec 04 14:43:33 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/morphism.ML
-    ID:         $Id$
     Author:     Makarius
 
 Abstract morphisms on formal entities.
@@ -17,21 +16,21 @@
 signature MORPHISM =
 sig
   include BASIC_MORPHISM
-  val var: morphism -> Name.binding * mixfix -> Name.binding * mixfix
-  val name: morphism -> Name.binding -> Name.binding
+  val var: morphism -> Binding.T * mixfix -> Binding.T * mixfix
+  val binding: morphism -> Binding.T -> Binding.T
   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: Name.binding -> Name.binding,
-    var: Name.binding * mixfix -> Name.binding * mixfix,
+   {binding: Binding.T -> Binding.T,
+    var: Binding.T * mixfix -> Binding.T * mixfix,
     typ: typ -> typ,
     term: term -> term,
     fact: thm list -> thm list} -> morphism
-  val name_morphism: (Name.binding -> Name.binding) -> morphism
-  val var_morphism: (Name.binding * mixfix -> Name.binding * mixfix) -> morphism
+  val binding_morphism: (Binding.T -> Binding.T) -> morphism
+  val var_morphism: (Binding.T * mixfix -> Binding.T * mixfix) -> morphism
   val typ_morphism: (typ -> typ) -> morphism
   val term_morphism: (term -> term) -> morphism
   val fact_morphism: (thm list -> thm list) -> morphism
@@ -46,15 +45,15 @@
 struct
 
 datatype morphism = Morphism of
- {name: Name.binding -> Name.binding,
-  var: Name.binding * mixfix -> Name.binding * mixfix,
+ {binding: Binding.T -> Binding.T,
+  var: Binding.T * mixfix -> Binding.T * mixfix,
   typ: typ -> typ,
   term: term -> term,
   fact: thm list -> thm list};
 
 type declaration = morphism -> Context.generic -> Context.generic;
 
-fun name (Morphism {name, ...}) = name;
+fun binding (Morphism {binding, ...}) = binding;
 fun var (Morphism {var, ...}) = var;
 fun typ (Morphism {typ, ...}) = typ;
 fun term (Morphism {term, ...}) = term;
@@ -64,19 +63,19 @@
 
 val morphism = Morphism;
 
-fun name_morphism name = morphism {name = name, var = I, typ = I, term = I, fact = I};
-fun var_morphism var = morphism {name = I, var = var, typ = I, term = I, fact = I};
-fun typ_morphism typ = morphism {name = I, var = I, typ = typ, term = I, fact = I};
-fun term_morphism term = morphism {name = I, var = I, typ = I, term = term, fact = I};
-fun fact_morphism fact = morphism {name = I, var = I, typ = I, term = I, fact = fact};
-fun thm_morphism thm = morphism {name = I, var = I, typ = I, term = I, fact = map thm};
+fun binding_morphism binding = morphism {binding = binding, var = I, typ = I, term = I, fact = I};
+fun var_morphism var = morphism {binding = I, var = var, typ = I, term = I, fact = I};
+fun typ_morphism typ = morphism {binding = I, var = I, typ = typ, term = I, fact = I};
+fun term_morphism term = morphism {binding = I, var = I, typ = I, term = term, fact = I};
+fun fact_morphism fact = morphism {binding = I, var = I, typ = I, term = I, fact = fact};
+fun thm_morphism thm = morphism {binding = I, var = I, typ = I, term = I, fact = map thm};
 
-val identity = morphism {name = I, var = I, typ = I, term = I, fact = I};
+val identity = morphism {binding = I, var = I, typ = I, term = I, fact = I};
 
 fun compose
-    (Morphism {name = name1, var = var1, typ = typ1, term = term1, fact = fact1})
-    (Morphism {name = name2, var = var2, typ = typ2, term = term2, fact = fact2}) =
-  morphism {name = name1 o name2, var = var1 o var2,
+    (Morphism {binding = binding1, var = var1, typ = typ1, term = term1, fact = fact1})
+    (Morphism {binding = binding2, var = var2, typ = typ2, term = term2, fact = fact2}) =
+  morphism {binding = binding1 o binding2, var = var1 o var2,
     typ = typ1 o typ2, term = term1 o term2, fact = fact1 o fact2};
 
 fun phi1 $> phi2 = compose phi2 phi1;