diff -r 6104514a1f5f -r f5e6932d0500 src/HOL/Extraction/Higman.thy
--- a/src/HOL/Extraction/Higman.thy	Mon Jul 16 09:29:02 2007 +0200
+++ b/src/HOL/Extraction/Higman.thy	Mon Jul 16 09:29:03 2007 +0200
@@ -409,12 +409,11 @@
   arbitrary_LT \<equiv> arbitrary_LT'
   arbitrary_TT \<equiv> arbitrary_TT'
 
-code_gen higman_idx in SML
+code_gen higman_idx in SML to Higman
 
 ML {*
 local
-  open ROOT.Higman
-  open ROOT.Nat
+  open Higman
 in
 
 val a = 16807.0;