src/Pure/morphism.ML
changeset 37216 3165bc303f66
parent 29605 f2924219125e
child 45289 25e9e7f527b4
--- 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;