# HG changeset patch
# User wenzelm
# Date 1164310408 -3600
# Node ID c73faa8e98aa85a623a1ddb374e6da01e54b1c69
# Parent  574e63799847a0c07f4b0980d9d031052a441751
added name/var/typ/term/thm_morphism;
removed transfer;

diff -r 574e63799847 -r c73faa8e98aa src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Thu Nov 23 20:33:25 2006 +0100
+++ b/src/Pure/morphism.ML	Thu Nov 23 20:33:28 2006 +0100
@@ -27,9 +27,13 @@
     typ: typ -> typ,
     term: term -> term,
     thm: thm -> thm} -> morphism
-  val comp: morphism -> morphism -> morphism
+  val name_morphism: (string -> string) -> morphism
+  val var_morphism: (string * mixfix -> string * mixfix) -> morphism
+  val typ_morphism: (typ -> typ) -> morphism
+  val term_morphism: (term -> term) -> morphism
+  val thm_morphism: (thm -> thm) -> morphism
   val identity: morphism
-  val transfer: theory -> morphism
+  val comp: morphism -> morphism -> morphism
 end;
 
 structure Morphism: MORPHISM =
@@ -50,6 +54,14 @@
 
 val morphism = Morphism;
 
+fun name_morphism name = morphism {name = name, var = I, typ = I, term = I, thm = I};
+fun var_morphism var = morphism {name = I, var = var, typ = I, term = I, thm = I};
+fun typ_morphism typ = morphism {name = I, var = I, typ = typ, term = I, thm = I};
+fun term_morphism term = morphism {name = I, var = I, typ = I, term = term, thm = I};
+fun thm_morphism thm = morphism {name = I, var = I, typ = I, term = I, thm = thm};
+
+val identity = morphism {name = I, var = I, typ = I, term = I, thm = I};
+
 fun comp
     (Morphism {name = name1, var = var1, typ = typ1, term = term1, thm = thm1})
     (Morphism {name = name2, var = var2, typ = typ2, term = term2, thm = thm2}) =
@@ -58,12 +70,7 @@
 
 fun phi1 $> phi2 = comp phi2 phi1;
 
-val identity = morphism {name = I, var = I, typ = I, term = I, thm = I};
-
-fun transfer thy = morphism {name = I, var = I, typ = I, term = I, thm = Thm.transfer thy};
-
 end;
 
 structure BasicMorphism: BASIC_MORPHISM = Morphism;
 open BasicMorphism;
-