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