diff -r 91dfe7dccfdf -r 3165bc303f66 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Mon May 31 19:36:13 2010 +0200
+++ b/src/Pure/morphism.ML	Mon May 31 21:06:57 2010 +0200
@@ -79,5 +79,5 @@
 
 end;
 
-structure BasicMorphism: BASIC_MORPHISM = Morphism;
-open BasicMorphism;
+structure Basic_Morphism: BASIC_MORPHISM = Morphism;
+open Basic_Morphism;