1.1 --- a/src/HOL/Import/HOL4/Template/GenHOL4Base.thy	Sat Mar 03 23:42:56 2012 +0100
     1.2 +++ b/src/HOL/Import/HOL4/Template/GenHOL4Base.thy	Sat Mar 03 23:43:21 2012 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4  *)
     1.5  
     1.6  theory GenHOL4Base
     1.7 -imports "../../HOL4Syntax" "../Compatibility"
     1.8 +imports "../../Importer" "../Compatibility"
     1.9  begin
    1.10  
    1.11  import_segment "hol4"
    1.12 @@ -11,7 +11,7 @@
    1.13  setup_dump "../Generated" "HOL4Base"
    1.14  
    1.15  append_dump {*theory HOL4Base
    1.16 -imports "../../HOL4Syntax" "../Compatibility"
    1.17 +imports "../../Importer" "../Compatibility"
    1.18  begin
    1.19  *}
    1.20  
    1.21 @@ -31,9 +31,9 @@
    1.22    "~"             > HOL.Not
    1.23    COND            > HOL.If
    1.24    bool_case       > Product_Type.bool.bool_case
    1.25 -  ONE_ONE         > HOL4Setup.ONE_ONE
    1.26 +  ONE_ONE         > Importer.ONE_ONE
    1.27    ONTO            > Fun.surj
    1.28 -  TYPE_DEFINITION > HOL4Setup.TYPE_DEFINITION
    1.29 +  TYPE_DEFINITION > Importer.TYPE_DEFINITION
    1.30    LET             > Compatibility.LET;
    1.31  
    1.32  ignore_thms