
diff -r a9ceeb182cfc -r 54cc492d80a9 src/HOL/Extraction/Higman.thy
--- a/src/HOL/Extraction/Higman.thy	Mon Nov 27 12:12:18 2006 +0100
+++ b/src/HOL/Extraction/Higman.thy	Mon Nov 27 13:42:30 2006 +0100
@@ -337,7 +337,7 @@
 end;
 *}
 
-code_gen good_prefix (SML *)
+code_gen good_prefix (SML #)
 
 ML {*
 local




