diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Extraction/Higman.thy
--- a/src/HOL/Extraction/Higman.thy	Sun May 06 21:49:44 2007 +0200
+++ b/src/HOL/Extraction/Higman.thy	Sun May 06 21:50:17 2007 +0200
@@ -406,7 +406,7 @@
   arbitrary_LT \<equiv> arbitrary_LT'
   arbitrary_TT \<equiv> arbitrary_TT'
 
-code_gen higman_idx (SML #)
+code_gen higman_idx in SML
 
 ML {*
 local