--- a/src/Pure/General/scan.ML Mon May 31 19:36:13 2010 +0200
+++ b/src/Pure/General/scan.ML Mon May 31 21:06:57 2010 +0200
@@ -322,5 +322,5 @@
end;
-structure BasicScan: BASIC_SCAN = Scan;
-open BasicScan;
+structure Basic_Scan: BASIC_SCAN = Scan;
+open Basic_Scan;