# HG changeset patch
# User wenzelm
# Date 1175621057 -7200
# Node ID 3f00e937d1c98f13b4425ccb6e64fc0ab57e2baf
# Parent  f166a5416b3fd8b8313bf03062c1250ef05c6e14
renamed comp to compose (avoid clash with Alice keywords);

diff -r f166a5416b3f -r 3f00e937d1c9 src/Pure/morphism.ML
--- 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;