diff -r 72c77ea184e6 -r 81e5ec0a3cd0 src/HOL/Import/HOL_Light/Template/GenHOLLight.thy
--- a/src/HOL/Import/HOL_Light/Template/GenHOLLight.thy	Sat Mar 03 23:42:56 2012 +0100
+++ b/src/HOL/Import/HOL_Light/Template/GenHOLLight.thy	Sat Mar 03 23:43:21 2012 +0100
@@ -4,7 +4,7 @@
 *)
 
 theory GenHOLLight
-imports "../../HOL4Syntax" "../Compatibility"
+imports "../../Importer" "../Compatibility"
 begin
 
 import_segment "hollight"
@@ -12,7 +12,7 @@
 setup_dump "../Generated" "HOLLight"
 
 append_dump {*theory HOL4Base
-imports "../../HOL4Syntax" "../Compatibility"
+imports "../../Importer" "../Compatibility"
 begin
 *}