# HG changeset patch
# User haftmann
# Date 1330815784 -3600
# Node ID 9696218b02fea24dfc3ea7b386548c4f8626ea6a
# Parent  f21494dc0bf670bf184e5d01667390c2e278623d
avoid internal hol4 name references in generic importer code

diff -r f21494dc0bf6 -r 9696218b02fe src/HOL/Import/README
--- a/src/HOL/Import/README	Sat Mar 03 23:54:44 2012 +0100
+++ b/src/HOL/Import/README	Sun Mar 04 00:03:04 2012 +0100
@@ -2,7 +2,7 @@
 ATTENTION!  This is largely outdated.  The hint to PROOF_DIRS might be
 everything which is still relevant.
 
-All the files in this directory (except this README, HOL4.thy, and
+All the files in this directory (except this README, Importer.thy, and
 ROOT.ML) are automatically generated.  Edit the files in
 ../Generate-HOL and run "isabelle make HOL-Complex-Generate-HOL" in
 ~~/src/HOL, if something needs to be changed.
diff -r f21494dc0bf6 -r 9696218b02fe src/HOL/Import/import.ML
--- a/src/HOL/Import/import.ML	Sat Mar 03 23:54:44 2012 +0100
+++ b/src/HOL/Import/import.ML	Sun Mar 04 00:03:04 2012 +0100
@@ -37,11 +37,11 @@
                                NONE => fst (Replay.setup_int_thms thyname thy)
                              | SOME a => a
             val proof = snd (ProofKernel.import_proof thyname thmname thy) thy
-            val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy)
-            val thm = snd (ProofKernel.to_isa_thm hol4thm)
-            val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy
+            val importerthm = snd (Replay.replay_proof int_thms thyname thmname proof thy)
+            val thm = snd (ProofKernel.to_isa_thm importerthm)
+            val rew = ProofKernel.rewrite_importer_term (concl_of thm) thy
             val thm = Thm.equal_elim rew thm
-            val prew = ProofKernel.rewrite_hol4_term prem thy
+            val prew = ProofKernel.rewrite_importer_term prem thy
             val prem' = #2 (Logic.dest_equals (prop_of prew))
             val _ = message ("Import proved " ^ Display.string_of_thm ctxt thm)
             val thm = ProofKernel.disambiguate_frees thm
diff -r f21494dc0bf6 -r 9696218b02fe src/HOL/Import/import_rews.ML
--- a/src/HOL/Import/import_rews.ML	Sat Mar 03 23:54:44 2012 +0100
+++ b/src/HOL/Import/import_rews.ML	Sun Mar 04 00:03:04 2012 +0100
@@ -11,7 +11,7 @@
        | Generating of string
        | Replaying of string
 
-structure HOL4DefThy = Theory_Data
+structure Importer_DefThy = Theory_Data
 (
   type T = ImportStatus
   val empty = NoImport
@@ -36,7 +36,7 @@
 val get_import_segment = ImportSegment.get
 val set_import_segment = ImportSegment.put
 
-structure HOL4UNames = Theory_Data
+structure Importer_UNames = Theory_Data
 (
   type T = string list
   val empty = []
@@ -45,7 +45,7 @@
     | merge _ = error "Used names not empty during merge"
 )
 
-structure HOL4Dump = Theory_Data
+structure Importer_Dump = Theory_Data
 (
   type T = string * string * string list
   val empty = ("","",[])
@@ -54,7 +54,7 @@
     | merge _ = error "Dump data not empty during merge"
 )
 
-structure HOL4Moves = Theory_Data
+structure Importer_Moves = Theory_Data
 (
   type T = string Symtab.table
   val empty = Symtab.empty
@@ -62,7 +62,7 @@
   fun merge data = Symtab.merge (K true) data
 )
 
-structure HOL4Imports = Theory_Data
+structure Importer_Imports = Theory_Data
 (
   type T = string Symtab.table
   val empty = Symtab.empty
@@ -71,17 +71,17 @@
 )
 
 fun get_segment2 thyname thy =
-  Symtab.lookup (HOL4Imports.get thy) thyname
+  Symtab.lookup (Importer_Imports.get thy) thyname
 
 fun set_segment thyname segname thy =
     let
-        val imps = HOL4Imports.get thy
+        val imps = Importer_Imports.get thy
         val imps' = Symtab.update_new (thyname,segname) imps
     in
-        HOL4Imports.put imps' thy
+        Importer_Imports.put imps' thy
     end
 
-structure HOL4CMoves = Theory_Data
+structure Importer_CMoves = Theory_Data
 (
   type T = string Symtab.table
   val empty = Symtab.empty
@@ -89,7 +89,7 @@
   fun merge data = Symtab.merge (K true) data
 )
 
-structure HOL4Maps = Theory_Data
+structure Importer_Maps = Theory_Data
 (
   type T = string option StringPair.table
   val empty = StringPair.empty
@@ -97,7 +97,7 @@
   fun merge data = StringPair.merge (K true) data
 )
 
-structure HOL4Thms = Theory_Data
+structure Importer_Thms = Theory_Data
 (
   type T = holthm StringPair.table
   val empty = StringPair.empty
@@ -105,7 +105,7 @@
   fun merge data = StringPair.merge (K true) data
 )
 
-structure HOL4ConstMaps = Theory_Data
+structure Importer_ConstMaps = Theory_Data
 (
   type T = (bool * string * typ option) StringPair.table
   val empty = StringPair.empty
@@ -113,7 +113,7 @@
   fun merge data = StringPair.merge (K true) data
 )
 
-structure HOL4Rename = Theory_Data
+structure Importer_Rename = Theory_Data
 (
   type T = string StringPair.table
   val empty = StringPair.empty
@@ -121,7 +121,7 @@
   fun merge data = StringPair.merge (K true) data
 )
 
-structure HOL4DefMaps = Theory_Data
+structure Importer_DefMaps = Theory_Data
 (
   type T = string StringPair.table
   val empty = StringPair.empty
@@ -129,7 +129,7 @@
   fun merge data = StringPair.merge (K true) data
 )
 
-structure HOL4TypeMaps = Theory_Data
+structure Importer_TypeMaps = Theory_Data
 (
   type T = (bool * string) StringPair.table
   val empty = StringPair.empty
@@ -137,7 +137,7 @@
   fun merge data = StringPair.merge (K true) data
 )
 
-structure HOL4Pending = Theory_Data
+structure Importer_Pending = Theory_Data
 (
   type T = ((term * term) list * thm) StringPair.table
   val empty = StringPair.empty
@@ -145,7 +145,7 @@
   fun merge data = StringPair.merge (K true) data
 )
 
-structure HOL4Rewrites = Theory_Data
+structure Importer_Rewrites = Theory_Data
 (
   type T = thm list
   val empty = []
@@ -153,57 +153,57 @@
   val merge = Thm.merge_thms
 )
 
-val hol4_debug = Unsynchronized.ref false
-fun message s = if !hol4_debug then writeln s else ()
+val importer_debug = Unsynchronized.ref false
+fun message s = if !importer_debug then writeln s else ()
 
-fun add_hol4_rewrite (Context.Theory thy, th) =
+fun add_importer_rewrite (Context.Theory thy, th) =
     let
         val _ = message "Adding external rewrite"
         val th1 = th RS @{thm eq_reflection}
                   handle THM _ => th
-        val current_rews = HOL4Rewrites.get thy
+        val current_rews = Importer_Rewrites.get thy
         val new_rews = insert Thm.eq_thm th1 current_rews
-        val updated_thy  = HOL4Rewrites.put new_rews thy
+        val updated_thy  = Importer_Rewrites.put new_rews thy
     in
         (Context.Theory updated_thy,th1)
     end
-  | add_hol4_rewrite (context, th) = (context,
+  | add_importer_rewrite (context, th) = (context,
       (th RS @{thm eq_reflection} handle THM _ => th)
     );
 
-fun ignore_hol4 bthy bthm thy =
+fun ignore_importer bthy bthm thy =
     let
         val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm)
-        val curmaps = HOL4Maps.get thy
+        val curmaps = Importer_Maps.get thy
         val newmaps = StringPair.update_new ((bthy,bthm),NONE) curmaps
-        val upd_thy = HOL4Maps.put newmaps thy
+        val upd_thy = Importer_Maps.put newmaps thy
     in
         upd_thy
     end
 
-val opt_get_output_thy = #2 o HOL4Dump.get
+val opt_get_output_thy = #2 o Importer_Dump.get
 
 fun get_output_thy thy =
-    case #2 (HOL4Dump.get thy) of
+    case #2 (Importer_Dump.get thy) of
         "" => error "No theory file being output"
       | thyname => thyname
 
-val get_output_dir = #1 o HOL4Dump.get
+val get_output_dir = #1 o Importer_Dump.get
 
-fun add_hol4_move bef aft thy =
+fun add_importer_move bef aft thy =
     let
-        val curmoves = HOL4Moves.get thy
+        val curmoves = Importer_Moves.get thy
         val newmoves = Symtab.update_new (bef, aft) curmoves
     in
-        HOL4Moves.put newmoves thy
+        Importer_Moves.put newmoves thy
     end
 
-fun get_hol4_move bef thy =
-  Symtab.lookup (HOL4Moves.get thy) bef
+fun get_importer_move bef thy =
+  Symtab.lookup (Importer_Moves.get thy) bef
 
 fun follow_name thmname thy =
     let
-        val moves = HOL4Moves.get thy
+        val moves = Importer_Moves.get thy
         fun F thmname =
             case Symtab.lookup moves thmname of
                 SOME name => F name
@@ -212,20 +212,20 @@
         F thmname
     end
 
-fun add_hol4_cmove bef aft thy =
+fun add_importer_cmove bef aft thy =
     let
-        val curmoves = HOL4CMoves.get thy
+        val curmoves = Importer_CMoves.get thy
         val newmoves = Symtab.update_new (bef, aft) curmoves
     in
-        HOL4CMoves.put newmoves thy
+        Importer_CMoves.put newmoves thy
     end
 
-fun get_hol4_cmove bef thy =
-  Symtab.lookup (HOL4CMoves.get thy) bef
+fun get_importer_cmove bef thy =
+  Symtab.lookup (Importer_CMoves.get thy) bef
 
 fun follow_cname thmname thy =
     let
-        val moves = HOL4CMoves.get thy
+        val moves = Importer_CMoves.get thy
         fun F thmname =
             case Symtab.lookup moves thmname of
                 SOME name => F name
@@ -234,140 +234,140 @@
         F thmname
     end
 
-fun add_hol4_mapping bthy bthm isathm thy =
+fun add_importer_mapping bthy bthm isathm thy =
     let 
        (* val _ = writeln ("Before follow_name: "^isathm)  *)
       val isathm = follow_name isathm thy
        (* val _ = writeln ("Adding theorem map: " ^ bthy ^ "." ^ bthm ^ " --> " ^ isathm)*)
-        val curmaps = HOL4Maps.get thy
+        val curmaps = Importer_Maps.get thy
         val newmaps = StringPair.update_new ((bthy,bthm),SOME isathm) curmaps
-        val upd_thy = HOL4Maps.put newmaps thy
+        val upd_thy = Importer_Maps.put newmaps thy
     in
         upd_thy
     end;
 
-fun get_hol4_type_mapping bthy tycon thy =
+fun get_importer_type_mapping bthy tycon thy =
     let
-        val maps = HOL4TypeMaps.get thy
+        val maps = Importer_TypeMaps.get thy
     in
         StringPair.lookup maps (bthy,tycon)
     end
 
-fun get_hol4_mapping bthy bthm thy =
+fun get_importer_mapping bthy bthm thy =
     let
-        val curmaps = HOL4Maps.get thy
+        val curmaps = Importer_Maps.get thy
     in
         StringPair.lookup curmaps (bthy,bthm)
     end;
 
-fun add_hol4_const_mapping bthy bconst internal isaconst thy =
+fun add_importer_const_mapping bthy bconst internal isaconst thy =
     let
         val thy = case opt_get_output_thy thy of
                       "" => thy
                     | output_thy => if internal
-                                    then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
+                                    then add_importer_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
                                     else thy
         val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
-        val curmaps = HOL4ConstMaps.get thy
+        val curmaps = Importer_ConstMaps.get thy
         val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,NONE)) curmaps
-        val upd_thy = HOL4ConstMaps.put newmaps thy
+        val upd_thy = Importer_ConstMaps.put newmaps thy
     in
         upd_thy
     end;
 
-fun add_hol4_const_renaming bthy bconst newname thy =
+fun add_importer_const_renaming bthy bconst newname thy =
     let
-        val currens = HOL4Rename.get thy
+        val currens = Importer_Rename.get thy
         val _ = message ("Adding renaming " ^ bthy ^ "." ^ bconst ^ " -> " ^ newname)
         val newrens = StringPair.update_new ((bthy,bconst),newname) currens
-        val upd_thy = HOL4Rename.put newrens thy
+        val upd_thy = Importer_Rename.put newrens thy
     in
         upd_thy
     end;
 
-fun get_hol4_const_renaming bthy bconst thy =
+fun get_importer_const_renaming bthy bconst thy =
     let
-        val currens = HOL4Rename.get thy
+        val currens = Importer_Rename.get thy
     in
         StringPair.lookup currens (bthy,bconst)
     end;
 
-fun get_hol4_const_mapping bthy bconst thy =
+fun get_importer_const_mapping bthy bconst thy =
     let
-        val bconst = case get_hol4_const_renaming bthy bconst thy of
+        val bconst = case get_importer_const_renaming bthy bconst thy of
                          SOME name => name
                        | NONE => bconst
-        val maps = HOL4ConstMaps.get thy
+        val maps = Importer_ConstMaps.get thy
     in
         StringPair.lookup maps (bthy,bconst)
     end
 
-fun add_hol4_const_wt_mapping bthy bconst internal isaconst typ thy =
+fun add_importer_const_wt_mapping bthy bconst internal isaconst typ thy =
     let
         val thy = case opt_get_output_thy thy of
                       "" => thy
                     | output_thy => if internal
-                                    then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
+                                    then add_importer_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
                                     else thy
         val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
-        val curmaps = HOL4ConstMaps.get thy
+        val curmaps = Importer_ConstMaps.get thy
         val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,SOME typ)) curmaps
-        val upd_thy = HOL4ConstMaps.put newmaps thy
+        val upd_thy = Importer_ConstMaps.put newmaps thy
     in
         upd_thy
     end;
 
-fun add_hol4_type_mapping bthy bconst internal isaconst thy =
+fun add_importer_type_mapping bthy bconst internal isaconst thy =
     let
-        val curmaps = HOL4TypeMaps.get thy
+        val curmaps = Importer_TypeMaps.get thy
         val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
         val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps
                (* FIXME avoid handle x *)
                handle x => let val (_, isaconst') = the (StringPair.lookup curmaps (bthy, bconst)) in
                       warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end
-        val upd_thy = HOL4TypeMaps.put newmaps thy
+        val upd_thy = Importer_TypeMaps.put newmaps thy
     in
         upd_thy
     end;
 
-fun add_hol4_pending bthy bthm hth thy =
+fun add_importer_pending bthy bthm hth thy =
     let
         val thmname = Sign.full_bname thy bthm
         val _ = message ("Add pending " ^ bthy ^ "." ^ bthm)
-        val curpend = HOL4Pending.get thy
+        val curpend = Importer_Pending.get thy
         val newpend = StringPair.update_new ((bthy,bthm),hth) curpend
-        val upd_thy = HOL4Pending.put newpend thy
+        val upd_thy = Importer_Pending.put newpend thy
         val thy' = case opt_get_output_thy upd_thy of
-                       "" => add_hol4_mapping bthy bthm thmname upd_thy
+                       "" => add_importer_mapping bthy bthm thmname upd_thy
                      | output_thy =>
                        let
                            val new_thmname = output_thy ^ "." ^ bthy ^ "." ^ bthm
                        in
-                           upd_thy |> add_hol4_move thmname new_thmname
-                                   |> add_hol4_mapping bthy bthm new_thmname
+                           upd_thy |> add_importer_move thmname new_thmname
+                                   |> add_importer_mapping bthy bthm new_thmname
                        end
     in
         thy'
     end;
 
-fun get_hol4_theorem thyname thmname thy =
+fun get_importer_theorem thyname thmname thy =
   let
-    val isathms = HOL4Thms.get thy
+    val isathms = Importer_Thms.get thy
   in
     StringPair.lookup isathms (thyname,thmname)
   end;
 
-fun add_hol4_theorem thyname thmname hth =
+fun add_importer_theorem thyname thmname hth =
   let
     val _ = message ("Adding external theorem " ^ thyname ^ "." ^ thmname)
   in
-    HOL4Thms.map (StringPair.update_new ((thyname, thmname), hth))
+    Importer_Thms.map (StringPair.update_new ((thyname, thmname), hth))
   end;
 
-fun export_hol4_pending thy =
+fun export_importer_pending thy =
   let
-    val rews = HOL4Rewrites.get thy;
-    val pending = HOL4Pending.get thy;
+    val rews = Importer_Rewrites.get thy;
+    val pending = Importer_Pending.get thy;
     fun process ((bthy,bthm), hth as (_,thm)) thy =
       let
         val thm1 = rewrite_rule (map (Thm.transfer thy) rews) (Thm.transfer thy thm);
@@ -376,68 +376,68 @@
         thy
         |> Global_Theory.store_thm (Binding.name bthm, thm2)
         |> snd
-        |> add_hol4_theorem bthy bthm hth
+        |> add_importer_theorem bthy bthm hth
       end;
   in
     thy
     |> StringPair.fold process pending
-    |> HOL4Pending.put StringPair.empty
+    |> Importer_Pending.put StringPair.empty
   end;
 
 fun setup_dump (dir,thyname) thy =
-    HOL4Dump.put (dir,thyname,["(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)"]) thy
+    Importer_Dump.put (dir,thyname,["(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)"]) thy
 
 fun add_dump str thy =
     let
-        val (dir,thyname,curdump) = HOL4Dump.get thy
+        val (dir,thyname,curdump) = Importer_Dump.get thy
     in
-        HOL4Dump.put (dir,thyname,str::curdump) thy
+        Importer_Dump.put (dir,thyname,str::curdump) thy
     end
 
 fun flush_dump thy =
     let
-        val (dir,thyname,dumpdata) = HOL4Dump.get thy
+        val (dir,thyname,dumpdata) = Importer_Dump.get thy
         val os = TextIO.openOut (OS.Path.joinDirFile {dir=dir,
                                                       file=thyname ^ ".thy"})
         val _  = app (fn s => TextIO.output(os,s ^ "\n\n")) (rev dumpdata)
         val  _ = TextIO.closeOut os
     in
-        HOL4Dump.put ("","",[]) thy
+        Importer_Dump.put ("","",[]) thy
     end
 
 fun set_generating_thy thyname thy =
-    case HOL4DefThy.get thy of
-        NoImport => HOL4DefThy.put (Generating thyname) thy
+    case Importer_DefThy.get thy of
+        NoImport => Importer_DefThy.put (Generating thyname) thy
       | _ => error "Import already in progess"
 
 fun set_replaying_thy thyname thy =
-    case HOL4DefThy.get thy of
-        NoImport => HOL4DefThy.put (Replaying thyname) thy
+    case Importer_DefThy.get thy of
+        NoImport => Importer_DefThy.put (Replaying thyname) thy
       | _ => error "Import already in progess"
 
 fun clear_import_thy thy =
-    case HOL4DefThy.get thy of
+    case Importer_DefThy.get thy of
         NoImport => error "No import in progress"
-      | _ => HOL4DefThy.put NoImport thy
+      | _ => Importer_DefThy.put NoImport thy
 
 fun get_generating_thy thy =
-    case HOL4DefThy.get thy of
+    case Importer_DefThy.get thy of
         Generating thyname => thyname
       | _ => error "No theory being generated"
 
 fun get_replaying_thy thy =
-    case HOL4DefThy.get thy of
+    case Importer_DefThy.get thy of
         Replaying thyname => thyname
       | _ => error "No theory being replayed"
 
 fun get_import_thy thy =
-    case HOL4DefThy.get thy of
+    case Importer_DefThy.get thy of
         Replaying thyname => thyname
       | Generating thyname => thyname
       | _ => error "No theory being imported"
 
 fun should_ignore thyname thy thmname =
-    case get_hol4_mapping thyname thmname thy of
+    case get_importer_mapping thyname thmname thy of
         SOME NONE => true 
       | _ => false
 
@@ -468,13 +468,13 @@
         then case v
          of NONE => (bthm :: ign, map)
           | SOME w => (ign, (bthm, w) :: map)
-        else (ign, map)) (HOL4Maps.get thy) ([],[]);
+        else (ign, map)) (Importer_Maps.get thy) ([],[]);
     fun mk init = StringPair.fold
       (fn ((bthy, bthm), v) => if bthy = thyname then cons (bthm, v) else I) init [];
-    val constmaps = mk (HOL4ConstMaps.get thy);
-    val constrenames = mk (HOL4Rename.get thy);
-    val typemaps = mk (HOL4TypeMaps.get thy);
-    val defmaps = mk (HOL4DefMaps.get thy);
+    val constmaps = mk (Importer_ConstMaps.get thy);
+    val constrenames = mk (Importer_Rename.get thy);
+    val typemaps = mk (Importer_TypeMaps.get thy);
+    val defmaps = mk (Importer_DefMaps.get thy);
         fun new_name internal isa =
             if internal
             then
@@ -565,18 +565,18 @@
 
 fun set_used_names names thy =
     let
-        val unames = HOL4UNames.get thy
+        val unames = Importer_UNames.get thy
     in
         case unames of
-            [] => HOL4UNames.put names thy
+            [] => Importer_UNames.put names thy
           | _ => error "import_rews.set_used_names called on initialized data!"
     end
 
-val clear_used_names = HOL4UNames.put [];
+val clear_used_names = Importer_UNames.put [];
 
 fun get_defmap thyname const thy =
     let
-        val maps = HOL4DefMaps.get thy
+        val maps = Importer_DefMaps.get thy
     in
         StringPair.lookup maps (thyname,const)
     end
@@ -584,23 +584,23 @@
 fun add_defmap thyname const defname thy =
     let
         val _ = message ("Adding defmap " ^ thyname ^ "." ^ const ^ " --> " ^ defname)
-        val maps = HOL4DefMaps.get thy
+        val maps = Importer_DefMaps.get thy
         val maps' = StringPair.update_new ((thyname,const),defname) maps
-        val thy' = HOL4DefMaps.put maps' thy
+        val thy' = Importer_DefMaps.put maps' thy
     in
         thy'
     end
 
 fun get_defname thyname name thy =
     let
-        val maps = HOL4DefMaps.get thy
+        val maps = Importer_DefMaps.get thy
         fun F dname = (dname,add_defmap thyname name dname thy)
     in
         case StringPair.lookup maps (thyname,name) of
             SOME thmname => (thmname,thy)
           | NONE =>
             let
-                val used = HOL4UNames.get thy
+                val used = Importer_UNames.get thy
                 val defname = Thm.def_name name
                 val pdefname = name ^ "_primdef"
             in
@@ -624,16 +624,16 @@
 
 local
     fun initial_maps thy =
-        thy |> add_hol4_type_mapping "min" "bool" false @{type_name bool}
-            |> add_hol4_type_mapping "min" "fun" false "fun"
-            |> add_hol4_type_mapping "min" "ind" false @{type_name ind}
-            |> add_hol4_const_mapping "min" "=" false @{const_name HOL.eq}
-            |> add_hol4_const_mapping "min" "==>" false @{const_name HOL.implies}
-            |> add_hol4_const_mapping "min" "@" false @{const_name "Eps"}
+        thy |> add_importer_type_mapping "min" "bool" false @{type_name bool}
+            |> add_importer_type_mapping "min" "fun" false "fun"
+            |> add_importer_type_mapping "min" "ind" false @{type_name ind}
+            |> add_importer_const_mapping "min" "=" false @{const_name HOL.eq}
+            |> add_importer_const_mapping "min" "==>" false @{const_name HOL.implies}
+            |> add_importer_const_mapping "min" "@" false @{const_name "Eps"}
 in
-val hol4_setup =
+val importer_setup =
   initial_maps #>
   Attrib.setup @{binding import_rew}
-    (Scan.succeed (Thm.mixed_attribute add_hol4_rewrite)) "external rewrite rule"
+    (Scan.succeed (Thm.mixed_attribute add_importer_rewrite)) "external rewrite rule"
 
 end
diff -r f21494dc0bf6 -r 9696218b02fe src/HOL/Import/import_syntax.ML
--- a/src/HOL/Import/import_syntax.ML	Sat Mar 03 23:54:44 2012 +0100
+++ b/src/HOL/Import/import_syntax.ML	Sun Mar 04 00:03:04 2012 +0100
@@ -2,7 +2,7 @@
     Author:     Sebastian Skalberg (TU Muenchen)
 *)
 
-signature HOL4_IMPORT_SYNTAX =
+signature IMPORTER_IMPORT_SYNTAX =
 sig
     val import_segment: (theory -> theory) parser
     val import_theory : (theory -> theory) parser
@@ -22,7 +22,7 @@
     val setup        : unit -> unit
 end
 
-structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX =
+structure Importer_Import_Syntax :> IMPORTER_IMPORT_SYNTAX =
 struct
 
 (* Parsers *)
@@ -51,7 +51,7 @@
                     |> set_used_names facts
                     |> replay 
                     |> clear_used_names
-                    |> export_hol4_pending
+                    |> export_importer_pending
                     |> Sign.parent_path
                     |> dump_import_thy thyname
                     |> add_dump ";end_setup"
@@ -63,7 +63,7 @@
                                       let
                                           val thyname = get_import_thy thy
                                       in
-                                          Library.foldl (fn (thy,thmname) => ignore_hol4 thyname thmname thy) (thy,ignored)
+                                          Library.foldl (fn (thy,thmname) => ignore_importer thyname thmname thy) (thy,ignored)
                                       end)
 
 val thm_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
@@ -72,7 +72,7 @@
                                    let
                                        val thyname = get_import_thy thy
                                    in
-                                       Library.foldl (fn (thy,(hol,isa)) => add_hol4_mapping thyname hol isa thy) (thy,thmmaps)
+                                       Library.foldl (fn (thy,(hol,isa)) => add_importer_mapping thyname hol isa thy) (thy,thmmaps)
                                    end)
 
 val type_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
@@ -81,7 +81,7 @@
                                     let
                                         val thyname = get_import_thy thy
                                     in
-                                        Library.foldl (fn (thy,(hol,isa)) => add_hol4_type_mapping thyname hol false isa thy) (thy,typmaps)
+                                        Library.foldl (fn (thy,(hol,isa)) => add_importer_type_mapping thyname hol false isa thy) (thy,typmaps)
                                     end)
 
 val def_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
@@ -99,7 +99,7 @@
                                         let
                                             val thyname = get_import_thy thy
                                         in
-                                            Library.foldl (fn (thy,(hol,isa)) => add_hol4_const_renaming thyname hol isa thy) (thy,renames)
+                                            Library.foldl (fn (thy,(hol,isa)) => add_importer_const_renaming thyname hol isa thy) (thy,renames)
                                         end)
                                                                                                                                       
 val const_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))
@@ -108,8 +108,8 @@
                                      let
                                          val thyname = get_import_thy thy
                                      in
-                                         Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol false isa thy
-                                                 | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
+                                         Library.foldl (fn (thy,((hol,isa),NONE)) => add_importer_const_mapping thyname hol false isa thy
+                                                 | (thy,((hol,isa),SOME ty)) => add_importer_const_wt_mapping thyname hol false isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
                                      end)
 
 val const_moves = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))
@@ -118,8 +118,8 @@
                                       let
                                           val thyname = get_import_thy thy
                                       in
-                                          Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol true isa thy
-                                                  | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
+                                          Library.foldl (fn (thy,((hol,isa),NONE)) => add_importer_const_mapping thyname hol true isa thy
+                                                  | (thy,((hol,isa),SOME ty)) => add_importer_const_wt_mapping thyname hol true isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
                                       end)
 
 fun import_thy location s =
@@ -172,7 +172,7 @@
                        >>
                        (fn (location, thyname) =>
                         fn thy =>
-                           (case HOL4DefThy.get thy of
+                           (case Importer_DefThy.get thy of
                                 NoImport => thy
                               | Generating _ => error "Currently generating a theory!"
                               | Replaying _ => thy |> clear_import_thy)
diff -r f21494dc0bf6 -r 9696218b02fe src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Sat Mar 03 23:54:44 2012 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Sun Mar 04 00:03:04 2012 +0100
@@ -60,7 +60,7 @@
     val content_of : proof -> proof_content
     val import_proof : string -> string -> theory -> (theory -> term) option * (theory -> proof)
 
-    val rewrite_hol4_term: Term.term -> theory -> Thm.thm
+    val rewrite_importer_term: Term.term -> theory -> Thm.thm
 
     val type_of : term -> hol_type
 
@@ -330,14 +330,14 @@
     end
 
 fun intern_const_name thyname const thy =
-    case get_hol4_const_mapping thyname const thy of
+    case get_importer_const_mapping thyname const thy of
         SOME (_,cname,_) => cname
-      | NONE => (case get_hol4_const_renaming thyname const thy of
+      | NONE => (case get_importer_const_renaming thyname const thy of
                      SOME cname => Sign.intern_const thy (thyname ^ "." ^ cname)
                    | NONE => Sign.intern_const thy (thyname ^ "." ^ const))
 
 fun intern_type_name thyname const thy =
-    case get_hol4_type_mapping thyname const thy of
+    case get_importer_type_mapping thyname const thy of
         SOME (_,cname) => cname
       | NONE => Sign.intern_const thy (thyname ^ "." ^ const)
 
@@ -357,7 +357,7 @@
 fun prim_mk_const thy Thy Nam =
     let
       val name = intern_const_name Thy Nam thy
-      val cmaps = HOL4ConstMaps.get thy
+      val cmaps = Importer_ConstMaps.get thy
     in
       case StringPair.lookup cmaps (Thy,Nam) of
         SOME(_,_,SOME ty) => Const(name,ty)
@@ -585,7 +585,7 @@
             case get_segment2 thyname thy of
                 SOME seg => seg
               | NONE => get_import_segment thy
-        val path = space_explode ":" (getenv "HOL4_PROOFS")
+        val path = space_explode ":" (getenv "IMPORTER_PROOFS")
         fun find [] = NONE
           | find (p::ps) =
             (let
@@ -1081,12 +1081,12 @@
 fun if_debug f x = if !debug then f x else ()
 val message = if_debug writeln
 
-fun get_hol4_thm thyname thmname thy =
-    case get_hol4_theorem thyname thmname thy of
+fun get_importer_thm thyname thmname thy =
+    case get_importer_theorem thyname thmname thy of
         SOME hth => SOME (HOLThm hth)
       | NONE =>
         let
-            val pending = HOL4Pending.get thy
+            val pending = Importer_Pending.get thy
         in
             case StringPair.lookup pending (thyname,thmname) of
                 SOME hth => SOME (HOLThm hth)
@@ -1112,30 +1112,30 @@
     end
     handle _ => NONE  (* FIXME avoid handle _ *)
 
-fun rewrite_hol4_term t thy =
+fun rewrite_importer_term t thy =
     let
-        val import_rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
-        val hol4ss = Simplifier.global_context thy empty_ss addsimps import_rews1
+        val import_rews1 = map (Thm.transfer thy) (Importer_Rewrites.get thy)
+        val importerss = Simplifier.global_context thy empty_ss addsimps import_rews1
     in
-        Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t))
+        Thm.transfer thy (Simplifier.full_rewrite importerss (cterm_of thy t))
     end
 
-fun get_isabelle_thm thyname thmname hol4conc thy =
+fun get_isabelle_thm thyname thmname importerconc thy =
     let
-        val (info,hol4conc') = disamb_term hol4conc
-        val i2h_conc = Thm.symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
+        val (info,importerconc') = disamb_term importerconc
+        val i2h_conc = Thm.symmetric (rewrite_importer_term (HOLogic.mk_Trueprop importerconc') thy)
         val isaconc =
             case concl_of i2h_conc of
                 Const("==",_) $ lhs $ _ => lhs
               | _ => error "get_isabelle_thm" "Bad rewrite rule"
         val _ = (message "Original conclusion:";
-                 if_debug prin hol4conc';
+                 if_debug prin importerconc';
                  message "Modified conclusion:";
                  if_debug prin isaconc)
 
         fun mk_res th = HOLThm (rens_of info, Thm.equal_elim i2h_conc th)
     in
-        case get_hol4_mapping thyname thmname thy of
+        case get_importer_mapping thyname thmname thy of
             SOME (SOME thmname) =>
             let
                 val th1 = (SOME (Global_Theory.get_thm thy thmname)
@@ -1167,8 +1167,8 @@
                     SOME (isaname,th) =>
                     let
                         val hth as HOLThm args = mk_res th
-                        val thy' =  thy |> add_hol4_theorem thyname thmname args
-                                        |> add_hol4_mapping thyname thmname isaname
+                        val thy' =  thy |> add_importer_theorem thyname thmname args
+                                        |> add_importer_mapping thyname thmname isaname
                     in
                         (thy',SOME hth)
                     end
@@ -1182,19 +1182,19 @@
             writeln ("Exception in get_isabelle_thm:\n" ^ ML_Compiler.exn_message e)) ();
           (thy,NONE))
 
-fun get_isabelle_thm_and_warn thyname thmname hol4conc thy =
+fun get_isabelle_thm_and_warn thyname thmname importerconc thy =
   let
-    val (a, b) = get_isabelle_thm thyname thmname hol4conc thy
+    val (a, b) = get_isabelle_thm thyname thmname importerconc thy
     fun warn () =
         let
-            val (info,hol4conc') = disamb_term hol4conc
-            val i2h_conc = Thm.symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
+            val (info,importerconc') = disamb_term importerconc
+            val i2h_conc = Thm.symmetric (rewrite_importer_term (HOLogic.mk_Trueprop importerconc') thy)
         in
             case concl_of i2h_conc of
                 Const("==",_) $ lhs $ _ =>
                 (warning ("Failed lookup of theorem '"^thmname^"':");
                  writeln "Original conclusion:";
-                 prin hol4conc';
+                 prin importerconc';
                  writeln "Modified conclusion:";
                  prin lhs)
               | _ => ()
@@ -1206,7 +1206,7 @@
   end
 
 fun get_thm thyname thmname thy =
-    case get_hol4_thm thyname thmname thy of
+    case get_importer_thm thyname thmname thy of
         SOME hth => (thy,SOME hth)
       | NONE => ((case import_proof_concl thyname thmname thy of
                       SOME f => get_isabelle_thm_and_warn thyname thmname (f thy) thy
@@ -1215,7 +1215,7 @@
                       | e as PK _ => (message "PK exception"; (thy,NONE)))
 
 fun rename_const thyname thy name =
-    case get_hol4_const_renaming thyname name thy of
+    case get_importer_const_renaming thyname name thy of
         SOME cname => cname
       | NONE => name
 
@@ -1236,9 +1236,9 @@
 fun intern_store_thm gen_output thyname thmname hth thy =
     let
         val (hth' as HOLThm (args as (_,th))) = norm_hthm thy hth
-        val rew = rewrite_hol4_term (concl_of th) thy
+        val rew = rewrite_importer_term (concl_of th) thy
         val th  = Thm.equal_elim rew th
-        val thy' = add_hol4_pending thyname thmname args thy
+        val thy' = add_importer_pending thyname thmname args thy
         val th = disambiguate_frees th
         val th = Object_Logic.rulify th
         val thy2 =
@@ -1791,7 +1791,7 @@
         val (info,rhs') = disamb_term rhs
         val ctype = type_of rhs'
         val csyn = mk_syn thy constname
-        val thy1 = case HOL4DefThy.get thy of
+        val thy1 = case Importer_DefThy.get thy of
                        Replaying _ => thy
                      | _ => Sign.add_consts_i [(Binding.name constname,ctype,csyn)] thy
         val eq = mk_defeq constname rhs' thy1
@@ -1800,9 +1800,9 @@
         val thm' = def_thm RS meta_eq_to_obj_eq_thm
         val (thy',th) = (thy2, thm')
         val fullcname = Sign.intern_const thy' constname
-        val thy'' = add_hol4_const_mapping thyname constname true fullcname thy'
+        val thy'' = add_importer_const_mapping thyname constname true fullcname thy'
         val (linfo,tm24) = disamb_term (mk_teq constname rhs' thy'')
-        val rew = rewrite_hol4_term eq thy''
+        val rew = rewrite_importer_term eq thy''
         val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew)))
         val thy22 =
           if Thm.def_name constname = thmname andalso not redeclared andalso csyn = NoSyn
@@ -1828,13 +1828,13 @@
                     | NONE => raise ERR "new_definition" "Bad conclusion"
         val fullname = Sign.full_bname thy22 thmname
         val thy22' = case opt_get_output_thy thy22 of
-                         "" => add_hol4_mapping thyname thmname fullname thy22
+                         "" => add_importer_mapping thyname thmname fullname thy22
                        | output_thy =>
                          let
                              val moved_thmname = output_thy ^ "." ^ thyname ^ "." ^ thmname
                          in
-                             thy22 |> add_hol4_move fullname moved_thmname
-                                   |> add_hol4_mapping thyname thmname moved_thmname
+                             thy22 |> add_importer_move fullname moved_thmname
+                                   |> add_importer_mapping thyname thmname moved_thmname
                          end
         val _ = message "new_definition:"
         val _ = if_debug pth hth
@@ -1843,7 +1843,7 @@
     end
 
 fun new_specification thyname thmname names hth thy =
-    case HOL4DefThy.get thy of
+    case Importer_DefThy.get thy of
         Replaying _ => (thy,hth)
       | _ =>
         let
@@ -1852,7 +1852,7 @@
             val names = map (rename_const thyname thy) names
             val _ = warning ("Introducing constants " ^ commas names)
             val (HOLThm(rens,th)) = norm_hthm thy hth
-            val thy1 = case HOL4DefThy.get thy of
+            val thy1 = case Importer_DefThy.get thy of
                            Replaying _ => thy
                          | _ =>
                            let
@@ -1892,7 +1892,7 @@
                                  (thy1,th)
             val res' = Thm.unvarify_global res
             val hth = HOLThm(rens,res')
-            val rew = rewrite_hol4_term (concl_of res') thy'
+            val rew = rewrite_importer_term (concl_of res') thy'
             val th  = Thm.equal_elim rew res'
             fun handle_const (name,thy) =
                 let
@@ -1938,7 +1938,7 @@
     val typedef_hol2hollight = @{thm typedef_hol2hollight}
 in
 fun new_type_definition thyname thmname tycname hth thy =
-    case HOL4DefThy.get thy of
+    case Importer_DefThy.get thy of
         Replaying _ => (thy,hth)
       | _ =>
         let
@@ -1960,14 +1960,14 @@
             val th3 = (#type_definition (#2 typedef_info)) RS typedef_hol2hol4
 
             val fulltyname = Sign.intern_type thy' tycname
-            val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
+            val thy'' = add_importer_type_mapping thyname tycname true fulltyname thy'
 
             val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th3))
             val _ = if has_ren hth' then warning ("Theorem " ^ thmname ^ " needs variable-disambiguating")
                     else ()
-            val thy4 = add_hol4_pending thyname thmname args thy''
+            val thy4 = add_importer_pending thyname thmname args thy''
 
-            val rew = rewrite_hol4_term (concl_of td_th) thy4
+            val rew = rewrite_importer_term (concl_of td_th) thy4
             val th  = Thm.equal_elim rew (Thm.transfer thy4 td_th)
             val c   = case HOLogic.dest_Trueprop (prop_of th) of
                           Const(@{const_name Ex},exT) $ P =>
@@ -1987,7 +1987,7 @@
             val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " "
                                  ^ (string_of_mixfix tsyn) ^ "\n  by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4
 
-            val thy6 = add_dump ("lemmas " ^ thmname ^ " = typedef_hol2hol4 [OF type_definition_" ^ tycname ^ "]") thy5
+            val thy6 = add_dump ("lemmas " ^ thmname ^ " = typedef_hol2importer [OF type_definition_" ^ tycname ^ "]") thy5
 
             val _ = message "RESULT:"
             val _ = if_debug pth hth'
@@ -2004,7 +2004,7 @@
     end
 
 fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy =
-    case HOL4DefThy.get thy of
+    case Importer_DefThy.get thy of
         Replaying _ => (thy,
           HOLThm([], Global_Theory.get_thm thy (thmname^"_@intern")) handle ERROR _ => hth)
       | _ =>
@@ -2042,12 +2042,12 @@
             val _ = null (Thm.fold_terms Term.add_vars th4 []) orelse
               raise ERR "type_introduction" "no term variables expected any more"
             val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname)
-            val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
+            val thy'' = add_importer_type_mapping thyname tycname true fulltyname thy'
             val _ = message "step 4"
             val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4))
-            val thy4 = add_hol4_pending thyname thmname args thy''
+            val thy4 = add_importer_pending thyname thmname args thy''
 
-            val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *)
+            val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_importer_term P thy4))) *)
             val c   =
                 let
                     val PT = type_of P'