--- 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