src/Pure/morphism.ML
changeset 22571 3f00e937d1c9
parent 22235 6eac7f7c3294
child 22670 c803b2696ada
--- a/src/Pure/morphism.ML	Tue Apr 03 19:24:16 2007 +0200
+++ b/src/Pure/morphism.ML	Tue Apr 03 19:24:17 2007 +0200
@@ -36,7 +36,7 @@
   val fact_morphism: (thm list -> thm list) -> morphism
   val thm_morphism: (thm -> thm) -> morphism
   val identity: morphism
-  val comp: morphism -> morphism -> morphism
+  val compose: morphism -> morphism -> morphism
 end;
 
 structure Morphism: MORPHISM =
@@ -68,13 +68,13 @@
 
 val identity = morphism {name = I, var = I, typ = I, term = I, fact = I};
 
-fun comp
+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,
     typ = typ1 o typ2, term = term1 o term2, fact = fact1 o fact2};
 
-fun phi1 $> phi2 = comp phi2 phi1;
+fun phi1 $> phi2 = compose phi2 phi1;
 
 end;