# HG changeset patch
# User wenzelm
# Date 1194556783 -3600
# Node ID 6ea18fd1105834a6e61cb576610f71ad6b8aa8a0
# Parent  059c03630d6ef676afcda1e0d63a3209a568364e
avoid "import" as identifier, which is a keyword in Alice;

diff -r 059c03630d6e -r 6ea18fd11058 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Nov 08 20:52:27 2007 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Nov 08 22:19:43 2007 +0100
@@ -444,10 +444,10 @@
 fun get_local_registrations ctxt = get_registrations (Context.Proof ctxt);
 
 
-fun get_registration ctxt import (name, ps) =
+fun get_registration ctxt imprt (name, ps) =
   case Symtab.lookup (RegistrationsData.get ctxt) name of
       NONE => NONE
-    | SOME reg => Registrations.lookup (Context.theory_of ctxt) (reg, (ps, import));
+    | SOME reg => Registrations.lookup (Context.theory_of ctxt) (reg, (ps, imprt));
 
 fun get_global_registration thy = get_registration (Context.Theory thy);
 fun get_local_registration ctxt = get_registration (Context.Proof ctxt);
@@ -1606,7 +1606,7 @@
    registration; requires parameters and flattened list of identifiers
    instead of recomputing it from the target *)
 
-fun collect_global_witnesses thy import parms ids vts = let
+fun collect_global_witnesses thy imprt parms ids vts = let
     val ts = map Logic.unvarify vts;
     val (parms, parmTs) = split_list parms;
     val parmvTs = map Logic.varifyT parmTs;
@@ -1619,11 +1619,11 @@
     val inst = Symtab.make (parms ~~ ts);
     val inst_ids = map (apfst (apsnd vinst_names)) ids;
     val assumed_ids' = map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE) inst_ids;
-    val wits = maps (#2 o the o get_global_registration thy import) assumed_ids';
+    val wits = maps (#2 o the o get_global_registration thy imprt) assumed_ids';
 
     val ids' = map fst inst_ids;
     val eqns =
-      fold_map (join_eqns (get_global_registration thy import) I (ProofContext.init thy))
+      fold_map (join_eqns (get_global_registration thy imprt) I (ProofContext.init thy))
         ids' Termtab.empty |> snd |> Termtab.dest |> map snd;
   in ((tinst, inst), wits, eqns) end;
 
@@ -2186,12 +2186,12 @@
                | _ => error "internal: illegal export in interpretation")
       |> Vartab.make;
     val dom = fold Term.add_frees res [] |> map Free;
-    val import = dom |> map (fn x => (Morphism.term export x, x))
+    val imprt = dom |> map (fn x => (Morphism.term export x, x))
       |> map_filter (fn (Free _, _) => NONE  (* fixed point of export *)
                | (Var y, x) => SOME (fst y, x)
                | _ => error "internal: illegal export in interpretation")
       |> Vartab.make;
-  in (((instT, inst), eqns''), (export, ((importT, domT), (import, dom)))) end;
+  in (((instT, inst), eqns''), (export, ((importT, domT), (imprt, dom)))) end;
 
 val read_instantiations = prep_instantiations Syntax.parse_term Syntax.parse_prop;
 val check_instantiations = prep_instantiations (K I) (K I);