First release of interpretation commands.

--- a/NEWS	Mon Apr 11 12:18:27 2005 +0200
+++ b/NEWS	Mon Apr 11 12:34:34 2005 +0200
@@ -222,6 +222,16 @@
   - Fixed parameter management in theorem generation for goals with "includes".
     INCOMPATIBILITY: rarely, the generated theorem statement is different.
 
+* Locales:  new commands for the interpretation of locale expressions
+  in theories (interpretation) and proof contexts (interpret).  These take an
+  instantiation of the locale parameters and compute proof obligations from
+  the instantiated specification.  After the obligations have been discharged,
+  the instantiated theorems of the locale are added to the theory or proof
+  context.  Interpretation is smart in that already active interpretations
+  do not occur in proof obligations, neither are instantiated theorems stored
+  in duplicate.
+  Use print_interps to inspect active interpretations of a particular locale.
+
 * New syntax
 
     <theorem_name> (<index>, ..., <index>-<index>, ...)

--- a/src/FOL/ex/LocaleTest.thy	Mon Apr 11 12:18:27 2005 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Mon Apr 11 12:34:34 2005 +0200
@@ -10,6 +10,13 @@
 
 theory LocaleTest = FOL:
 
+ML {* set quick_and_dirty *}    (* allow for thm command in batch mode *)
+ML {* set Toplevel.debug *}
+ML {* set show_hyps *}
+ML {* set show_sorts *}
+
+section {* interpretation *}
+
 (* interpretation input syntax *)
 
 locale L
@@ -26,8 +33,6 @@
 
 (* processing of locale expression *)
 
-ML {* reset show_hyps *}
-
 locale A = fixes a assumes asm_A: "a = a"
 
 locale (open) B = fixes b assumes asm_B [simp]: "b = b"
@@ -37,14 +42,15 @@
 
 locale D = A + B + fixes d defines def_D: "d == (a = b)"
 
-ML {* set show_sorts *}
+theorem (in A)
+  includes D
+  shows True ..
+
+theorem (in D) True ..
 
 typedecl i
 arities i :: "term"
 
-ML {* set Toplevel.debug *}
-
-ML {* set show_hyps *}
 
 interpretation p1: C ["X::'b" "Y::'b"] by (auto intro: A.intro C_axioms.intro)
   (* both X and Y get type 'b since 'b is the internal type of parameter b,
@@ -52,10 +58,10 @@
 
 print_interps A
 
-(* possible accesses
+(* possible accesses *)
 thm p1.a.asm_A thm LocaleTest.p1.a.asm_A
 thm LocaleTest.asm_A thm p1.asm_A
-*)
+
 
 (* without prefix *)
 
@@ -63,53 +69,211 @@
 
 print_interps A
 
-(* possible accesses
+(* possible accesses *)
 thm a.asm_A thm asm_A thm LocaleTest.a.asm_A thm LocaleTest.asm_A
-*)
+
 
 interpretation p2: D [X Y "Y = X"] by (auto intro: A.intro simp: eq_commute)
 
 print_interps D
 
-(*
 thm p2.a.asm_A
-*)
+
 
 interpretation p3: D [X Y] .
 
 (* duplicate: not registered *)
-(*
-thm p3.a.asm_A
-*)
+
+(* thm p3.a.asm_A *)
+
 
 print_interps A
 print_interps B
 print_interps C
 print_interps D
 
-(* not permitted *)
-(*
-interpretation p4: A ["x::?'a1"] apply (rule A.intro) apply rule done
-*)
+(* not permitted
+
+interpretation p4: A ["?x::?'a1"] apply (rule A.intro) apply rule done
+
 print_interps A
+*)
 
-(* without a prefix *)
-(* TODO!!!
-interpretation A [Z] apply - apply (auto intro: A.intro) done
-*)
+interpretation p10: D + D a' b' d' [X Y _ U V _] by (auto intro: A.intro)
+
+corollary (in D) th_x: True ..
+
+(* possible accesses: for each registration *)
+
+thm p2.th_x thm p3.th_x thm p10.th_x
+
+lemma (in D) th_y: "d == (a = b)" .
+
+thm p2.th_y thm p3.th_y thm p10.th_y
+
+lemmas (in D) th_z = th_y
+
+thm p2.th_z
+
+thm asm_A
+
+section {* Interpretation in proof contexts *}
 
 theorem True
 proof -
   fix alpha::i and beta::i and gamma::i
-  assume "A(alpha)"
+  have alpha_A: "A(alpha)" by (auto intro: A.intro)
   then interpret p5: A [alpha] .
   print_interps A
+  thm p5.asm_A
   interpret p6: C [alpha beta] by (auto intro: C_axioms.intro)
   print_interps A   (* p6 not added! *)
   print_interps C
 qed rule
 
-(* lemma "bla.bla": True by rule *)
+theorem (in A) True
+proof -
+  print_interps A
+  fix beta and gamma
+  interpret p9: D [a beta _]
+    (* no proof obligation for A !!! *)
+    apply - apply (rule refl) apply assumption done
+qed rule
 
 
+(* Definition involving free variable *)
+
+ML {* reset show_sorts *}
+
+locale E = fixes e defines e_def: "e(x) == x & x"
+  notes e_def2 = e_def
+
+lemma (in E) True thm e_def by fast
+
+interpretation p7: E ["(%x. x)"] by simp
+
+(* TODO: goal mustn't be beta-reduced here, is doesn't match meta-hyp *)
+
+thm p7.e_def2
+
+locale E' = fixes e defines e_def: "e == (%x. x & x)"
+  notes e_def2 = e_def
+
+interpretation p7': E' ["(%x. x)"] by simp
+
+thm p7'.e_def2
+
+(* Definition involving free variable in assm *)
+
+locale (open) F = fixes f assumes asm_F: "f --> x"
+  notes asm_F2 = asm_F
+
+interpretation p8: F ["False"] by fast
+
+thm p8.asm_F2
+
+subsection {* Locale without assumptions *}
+
+locale L1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]]
+
+lemma "[| P; Q |] ==> P & Q"
+proof -
+  interpret my: L1 .           txt {* No chained fact required. *}
+  assume Q and P               txt {* order reversed *}
+  then show "P & Q" ..         txt {* Applies @{thm my.rev_conjI}. *}
+qed
+
+locale L11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]]
+
+lemma "[| P; Q |] ==> P & Q"
+proof -
+  interpret [intro]: L11 .     txt {* Attribute supplied at instantiation. *}
+  assume Q and P
+  then show "P & Q" ..
+qed
+
+subsection {* Simple locale with assumptions *}
+
+consts bin :: "[i, i] => i" (infixl "#" 60)
+
+axioms i_assoc: "(x # y) # z = x # (y # z)"
+  i_comm: "x # y = y # x"
+
+locale L2 =
+  fixes OP (infixl "+" 60)
+  assumes assoc: "(x + y) + z = x + (y + z)"
+    and comm: "x + y = y + x"
+
+lemma (in L2) lcomm: "x + (y + z) = y + (x + z)"
+proof -
+  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
+  also have "... = (y + x) + z" by (simp add: comm)
+  also have "... = y + (x + z)" by (simp add: assoc)
+  finally show ?thesis .
+qed
+
+lemmas (in L2) AC = comm assoc lcomm
+
+lemma "(x::i) # y # z # w = y # x # w # z"
+proof -
+  interpret my: L2 ["op #"] by (rule L2.intro [of "op #", OF i_assoc i_comm])
+    txt {* Chained fact required to discharge assumptions of @{text L2}
+      and instantiate parameters. *}
+  show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
+qed
+
+subsection {* Nested locale with assumptions *}
+
+locale L3 =
+  fixes OP (infixl "+" 60)
+  assumes assoc: "(x + y) + z = x + (y + z)"
+
+locale L4 = L3 +
+  assumes comm: "x + y = y + x"
+
+lemma (in L4) lcomm: "x + (y + z) = y + (x + z)"
+proof -
+  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
+  also have "... = (y + x) + z" by (simp add: comm)
+  also have "... = y + (x + z)" by (simp add: assoc)
+  finally show ?thesis .
+qed
+
+lemmas (in L4) AC = comm assoc lcomm
+
+lemma "(x::i) # y # z # w = y # x # w # z"
+proof -
+  interpret my: L4 ["op #"]
+    by (auto intro: L3.intro L4_axioms.intro i_assoc i_comm)
+  show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
+qed
+
+subsection {* Locale with definition *}
+
+text {* This example is admittedly not very creative :-) *}
+
+locale L5 = L4 + var A +
+  defines A_def: "A == True"
+
+lemma (in L5) lem: A
+  by (unfold A_def) rule
+
+lemma "L5(op #) ==> True"
+proof -
+  assume "L5(op #)"
+  then interpret L5 ["op #"] by (auto intro: L5.axioms)
+  show ?thesis by (rule lem)  (* lem instantiated to True *)
+qed
+
+subsection {* Instantiation in a context with target *}
+
+lemma (in L4)
+  fixes A (infixl "$" 60)
+  assumes A: "L4(A)"
+  shows "(x::i) $ y $ z $ w = y $ x $ w $ z"
+proof -
+  from A interpret A: L4 ["A"] by (auto intro: L4.axioms)
+  show ?thesis by (simp only: A.OP.AC)
+qed
+
 end

--- a/src/HOL/Algebra/CRing.thy	Mon Apr 11 12:18:27 2005 +0200
+++ b/src/HOL/Algebra/CRing.thy	Mon Apr 11 12:34:34 2005 +0200
@@ -574,10 +574,28 @@
 
 locale ring_hom_cring = cring R + cring S + var h +
   assumes homh [simp, intro]: "h \<in> ring_hom R S"
+(*
   notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
     and hom_mult [simp] = ring_hom_mult [OF homh]
     and hom_add [simp] = ring_hom_add [OF homh]
     and hom_one [simp] = ring_hom_one [OF homh]
+*)
+
+lemma (in ring_hom_cring) hom_closed [simp, intro]:
+  "x \<in> carrier R ==> h x \<in> carrier S"
+  by (simp add: ring_hom_closed [OF homh])
+
+lemma (in ring_hom_cring) hom_mult [simp]:
+  "[| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
+  by (simp add: ring_hom_mult [OF homh])
+
+lemma (in ring_hom_cring) hom_add [simp]:
+  "[| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
+  by (simp add: ring_hom_add [OF homh])
+
+lemma (in ring_hom_cring) hom_one [simp]:
+  "h \<one> = \<one>\<^bsub>S\<^esub>"
+  by (simp add: ring_hom_one [OF homh])
 
 lemma (in ring_hom_cring) hom_zero [simp]:
   "h \<zero> = \<zero>\<^bsub>S\<^esub>"

--- a/src/HOL/Algebra/Group.thy	Mon Apr 11 12:18:27 2005 +0200
+++ b/src/HOL/Algebra/Group.thy	Mon Apr 11 12:34:34 2005 +0200
@@ -469,7 +469,7 @@
   apply (simp_all add: prems group_def group.l_inv)
   done
 
-text{*This alternative proof of the previous result demonstrates instantiate.
+text{*This alternative proof of the previous result demonstrates interpret.
    It uses @{text Prod.inv_equality} (available after instantiation) instead of
    @{text "group.inv_equality [OF DirProd_group]"}. *}
 lemma
@@ -478,9 +478,8 @@
       and h: "h \<in> carrier H"
   shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
 proof -
-  have "group (G \<times>\<times> H)"
-    by (blast intro: DirProd_group group.intro prems)
-  then instantiate Prod: group
+  interpret Prod: group ["G \<times>\<times> H"]
+    by (auto intro: DirProd_group group.intro group.axioms prems)
   show ?thesis by (simp add: Prod.inv_equality g h)
 qed
   
@@ -543,8 +542,19 @@
   @{term H}, with a homomorphism @{term h} between them*}
 locale group_hom = group G + group H + var h +
   assumes homh: "h \<in> hom G H"
+(*
   notes hom_mult [simp] = hom_mult [OF homh]
     and hom_closed [simp] = hom_closed [OF homh]
+CB: late binding problem?
+*)
+
+lemma (in group_hom) hom_mult [simp]:
+  "[| x \<in> carrier G; y \<in> carrier G |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
+  by (simp add: hom_mult [OF homh])
+
+lemma (in group_hom) hom_closed [simp]:
+  "x \<in> carrier G ==> h x \<in> carrier H"
+  by (simp add: hom_closed [OF homh])
 
 lemma (in group_hom) one_closed [simp]:
   "h \<one> \<in> carrier H"

--- a/src/HOL/Algebra/UnivPoly.thy	Mon Apr 11 12:18:27 2005 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Mon Apr 11 12:34:34 2005 +0200
@@ -1466,12 +1466,15 @@
   eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
 proof -
   assume S: "s \<in> carrier S" and R: "r \<in> carrier R"
+  from ring_hom_cring_P_S [OF S] interpret ring_hom_cring [P S "eval R S h s"]
+    by - (rule ring_hom_cring.axioms, assumption)+
+    (* why is simplifier invoked --- in done ??? *)
   from R S have "eval R S h s (monom P r n) =
     eval R S h s (monom P r 0 \<otimes>\<^bsub>P\<^esub> (monom P \<one> 1) (^)\<^bsub>P\<^esub> n)"
     by (simp del: monom_mult (* eval.hom_mult eval.hom_pow, delayed inst! *)
       add: monom_mult [THEN sym] monom_pow)
   also
-  from ring_hom_cring_P_S [OF S] instantiate eval: ring_hom_cring
+  (*  from ring_hom_cring_P_S [OF S] instantiate eval: ring_hom_cring *)
   from R S eval_monom1 have "... = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
     by (simp add: eval_const)
   finally show ?thesis .
@@ -1482,7 +1485,11 @@
   eval R S h s (r \<odot>\<^bsub>P\<^esub> p) = h r \<otimes>\<^bsub>S\<^esub> eval R S h s p"
 proof -
   assume S: "s \<in> carrier S" and R: "r \<in> carrier R" and P: "p \<in> carrier P"
+  from ring_hom_cring_P_S [OF S] interpret ring_hom_cring [P S "eval R S h s"]
+    by - (rule ring_hom_cring.axioms, assumption)+
+(*
   from ring_hom_cring_P_S [OF S] instantiate eval: ring_hom_cring
+*)
   from S R P show ?thesis
     by (simp add: monom_mult_is_smult [THEN sym] eval_const)
 qed
@@ -1503,20 +1510,20 @@
     and S: "s \<in> carrier S" and P: "p \<in> carrier P"
   shows "Phi p = Psi p"
 proof -
-  have Phi_hom: "ring_hom_cring P S Phi"
-    by (auto intro: ring_hom_cringI UP_cring S.cring Phi)
-  have Psi_hom: "ring_hom_cring P S Psi"
-    by (auto intro: ring_hom_cringI UP_cring S.cring Psi)
+  from UP_cring interpret cring [P] by - (rule cring.axioms, assumption)+
+  interpret Phi: ring_hom_cring [P S Phi]
+    by (auto intro: ring_hom_cring.axioms ring_hom_cringI UP_cring S.cring Phi)
+  interpret Psi: ring_hom_cring [P S Psi]
+    by (auto intro: ring_hom_cring.axioms ring_hom_cringI UP_cring S.cring Psi)
+
   have "Phi p =
       Phi (\<Oplus>\<^bsub>P \<^esub>i \<in> {..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 (^)\<^bsub>P\<^esub> i)"
     by (simp add: up_repr P S monom_mult [THEN sym] monom_pow del: monom_mult)
-  also 
-    from Phi_hom instantiate Phi: ring_hom_cring
-    from Psi_hom instantiate Psi: ring_hom_cring
-    have "... =
+  also
+  have "... =
       Psi (\<Oplus>\<^bsub>P \<^esub>i\<in>{..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 (^)\<^bsub>P\<^esub> i)"
     by (simp add: Phi Psi P S Pi_def comp_def)
-(* Without instantiate, the following command would have been necessary.
+(* Without interpret, the following command would have been necessary.
     by (simp add: ring_hom_cring.hom_finsum [OF Phi_hom]
       ring_hom_cring.hom_mult [OF Phi_hom]
       ring_hom_cring.hom_pow [OF Phi_hom] Phi

--- a/src/Pure/Isar/isar_thy.ML	Mon Apr 11 12:18:27 2005 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Mon Apr 11 12:34:34 2005 +0200
@@ -58,11 +58,17 @@
     -> bool -> theory -> ProofHistory.T
   val theorem_i: string -> (bstring * theory attribute list) *
     (term * (term list * term list)) -> bool -> theory -> ProofHistory.T
-  val multi_theorem: string -> (theory -> theory) -> bstring * Args.src list
+  val multi_theorem:
+    string -> (theory -> theory) -> 
+    (cterm list -> Proof.context -> Proof.context -> thm -> thm) ->
+    bstring * Args.src list
     -> Args.src Locale.element Locale.elem_expr list
     -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
     -> bool -> theory -> ProofHistory.T
-  val multi_theorem_i: string -> (theory -> theory) -> bstring * theory attribute list
+  val multi_theorem_i:
+    string -> (theory -> theory) ->  
+    (cterm list -> Proof.context -> Proof.context -> thm -> thm) ->
+    bstring * theory attribute list
     -> Locale.multi_attribute Locale.element_i Locale.elem_expr list
     -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
     -> bool -> theory -> ProofHistory.T
@@ -378,28 +384,33 @@
 
 in
 
-fun multi_theorem k thy_mod a elems concl int thy =
-  global_statement (Proof.multi_theorem k thy_mod NONE (apsnd (map (Attrib.global_attribute thy)) a)
+fun multi_theorem k thy_mod export a elems concl int thy =
+  global_statement (Proof.multi_theorem k thy_mod export NONE (apsnd (map (Attrib.global_attribute thy)) a)
     (map (Locale.map_attrib_elem_or_expr (Attrib.multi_attribute thy)) elems)) concl int thy;
 
-fun multi_theorem_i k thy_mod a = global_statement_i o Proof.multi_theorem_i k thy_mod NONE a;
+fun multi_theorem_i k thy_mod export a = global_statement_i o Proof.multi_theorem_i k thy_mod export NONE a;
 
 fun locale_multi_theorem k locale (name, atts) elems concl int thy =
-  global_statement (Proof.multi_theorem k I
+  global_statement (Proof.multi_theorem k I ProofContext.export_standard
       (SOME (locale, (map (Attrib.multi_attribute thy) atts,
           map (map (Attrib.multi_attribute thy) o snd o fst) concl)))
       (name, []) (map (Locale.map_attrib_elem_or_expr (Attrib.multi_attribute thy)) elems))
       (map (apfst (apsnd (K []))) concl) int thy;
 
 fun locale_multi_theorem_i k locale (name, atts) elems concl =
-  global_statement_i (Proof.multi_theorem_i k I (SOME (locale, (atts, map (snd o fst) concl)))
+  global_statement_i (Proof.multi_theorem_i k I ProofContext.export_standard
+      (SOME (locale, (atts, map (snd o fst) concl)))
       (name, []) elems) (map (apfst (apsnd (K []))) concl);
 
-fun theorem k (a, t) = multi_theorem k I a [] [(("", []), [t])];
-fun theorem_i k (a, t) = multi_theorem_i k I a [] [(("", []), [t])];
+fun theorem k (a, t) = multi_theorem k I ProofContext.export_standard
+       a [] [(("", []), [t])];
+fun theorem_i k (a, t) = multi_theorem_i k I ProofContext.export_standard
+       a [] [(("", []), [t])];
 
-fun smart_multi_theorem k NONE a elems = multi_theorem k I a elems
-  | smart_multi_theorem k (SOME locale) a elems = locale_multi_theorem k locale a elems;
+fun smart_multi_theorem k NONE a elems =
+      multi_theorem k I ProofContext.export_standard a elems
+  | smart_multi_theorem k (SOME locale) a elems =
+      locale_multi_theorem k locale a elems;
 
 val assume      = local_statement Proof.assume I;
 val assume_i    = local_statement_i Proof.assume_i I;
@@ -640,8 +651,10 @@
         (Locale.add_global_witness id thm' thy, thm')
       end;
   in
-    multi_theorem_i Drule.internalK activate ("", []) [] 
-      (map (fn (id as (n, _), props) => ((NameSpace.base n, [witness id]), 
+    multi_theorem_i Drule.internalK activate ProofContext.export_plain
+      ("", []) [] 
+      (map (fn ((n, ps), props) => 
+          ((NameSpace.base n, [witness (n, map Logic.varify ps)]), 
         map (fn prop => (prop, ([], []))) props)) propss) b thy'
   end;
 

--- a/src/Pure/Isar/locale.ML	Mon Apr 11 12:18:27 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Apr 11 12:34:34 2005 +0200
@@ -71,19 +71,26 @@
   val print_global_registrations: string -> theory -> unit
   val print_local_registrations: string -> context -> unit
 
-  val add_locale: bool -> bstring -> expr -> multi_attribute element list -> theory -> theory
-  val add_locale_i: bool -> bstring -> expr -> multi_attribute element_i list
-    -> theory -> theory
-  val smart_note_thmss: string -> (string * 'a) option ->
+  (* Storing results *)
+  val add_locale:
+    bool -> bstring -> expr -> multi_attribute element list -> theory -> theory
+  val add_locale_i:
+    bool -> bstring -> expr -> multi_attribute element_i list ->
+    theory -> theory
+  val smart_note_thmss:
+    string -> (string * 'a) option ->
     ((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
     theory -> theory * (bstring * thm list) list
-  val note_thmss: string -> xstring ->
+  val note_thmss:
+    string -> xstring ->
     ((bstring * multi_attribute list) * (thmref * multi_attribute list) list) list ->
     theory -> theory * (bstring * thm list) list
-  val note_thmss_i: string -> string ->
+  val note_thmss_i:
+    string -> string ->
     ((bstring * multi_attribute list) * (thm list * multi_attribute list) list) list ->
     theory -> theory * (bstring * thm list) list
-  val add_thmss: string -> ((string * thm list) * multi_attribute list) list ->
+  val add_thmss:
+    string -> string -> ((string * thm list) * multi_attribute list) list ->
     theory * context -> (theory * context) * (string * thm list) list
 
   (* Locale interpretation *)
@@ -232,8 +239,22 @@
 
 (* access registrations *)
 
+(* Ids of global registrations are varified,
+   Ids of local registrations are not.
+   Thms of registrations are never varified. *)
+
 (* retrieve registration from theory or context *)
 
+fun gen_get_registrations get thy_ctxt name =
+  case Symtab.lookup (get thy_ctxt, name) of
+      NONE => []
+    | SOME tab => Termlisttab.dest tab;
+
+val get_global_registrations =
+     gen_get_registrations (#3 o GlobalLocalesData.get);
+val get_local_registrations =
+     gen_get_registrations LocalLocalesData.get;
+
 fun gen_get_registration get thy_ctxt (name, ps) =
   case Symtab.lookup (get thy_ctxt, name) of
       NONE => NONE
@@ -271,6 +292,7 @@
          (space, locs, f regs)));
 val put_local_registration = gen_put_registration LocalLocalesData.map;
 
+(* TODO: needed? *)
 fun smart_put_registration id attn ctxt =
   (* ignore registration if already present in theory *)
      let
@@ -328,8 +350,14 @@
     val regs = get_regs thy_ctxt;
     val prt_term = Pretty.quote o Sign.pretty_term sg;
     fun prt_inst (ts, ((prfx, _), thms)) =
-      Pretty.block [Pretty.str prfx, Pretty.str ":", Pretty.brk 1,
-        Pretty.list "(" ")" (map prt_term ts)];
+         let
+           val pp_ts = Pretty.enclose "(" ")"
+             (Pretty.breaks (map prt_term ts));
+         in
+           if prfx = "" then Pretty.block [pp_ts]
+           else Pretty.block
+             [Pretty.str prfx, Pretty.str ":", Pretty.brk 1, pp_ts]
+         end;
     val loc_regs = Symtab.lookup (regs, loc_int);
   in
     (case loc_regs of
@@ -463,6 +491,114 @@
       Notes (map (apsnd (map (apfst (map (inst_thm ctxt env))))) facts);
 
 
+(* term and type instantiation, variant using symbol tables *)
+
+(* instantiate TFrees *)
+
+fun tinst_tab_type tinst T = if Symtab.is_empty tinst
+      then T
+      else Term.map_type_tfree
+        (fn (v as (x, _)) => getOpt (Symtab.lookup (tinst, x), (TFree v))) T;
+
+fun tinst_tab_term tinst t = if Symtab.is_empty tinst
+      then t
+      else Term.map_term_types (tinst_tab_type tinst) t;
+
+fun tinst_tab_thm sg tinst thm = if Symtab.is_empty tinst
+      then thm
+      else let
+          val cert = Thm.cterm_of sg;
+          val certT = Thm.ctyp_of sg;
+          val {hyps, prop, ...} = Thm.rep_thm thm;
+          val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
+          val tinst' = Symtab.dest tinst |>
+                List.filter (fn (a, _) => a mem_string tfrees);
+        in
+          if null tinst' then thm
+          else thm |> Drule.implies_intr_list (map cert hyps)
+            |> Drule.tvars_intr_list (map #1 tinst')
+            |> (fn (th, al) => th |> Thm.instantiate
+                ((map (fn (a, T) => (valOf (assoc (al, a)), certT T)) tinst'),
+                  []))
+            |> (fn th => Drule.implies_elim_list th
+                 (map (Thm.assume o cert o tinst_tab_term tinst) hyps))
+        end;
+
+fun tinst_tab_elem _ tinst (Fixes fixes) =
+      Fixes (map (fn (x, T, mx) => (x, Option.map (tinst_tab_type tinst) T, mx)) fixes)
+  | tinst_tab_elem _ tinst (Assumes asms) =
+      Assumes (map (apsnd (map (fn (t, (ps, qs)) =>
+        (tinst_tab_term tinst t,
+          (map (tinst_tab_term tinst) ps, map (tinst_tab_term tinst) qs))))) asms)
+  | tinst_tab_elem _ tinst (Defines defs) =
+      Defines (map (apsnd (fn (t, ps) =>
+        (tinst_tab_term tinst t, map (tinst_tab_term tinst) ps))) defs)
+  | tinst_tab_elem sg tinst (Notes facts) =
+      Notes (map (apsnd (map (apfst (map (tinst_tab_thm sg tinst))))) facts);
+
+(* instantiate TFrees and Frees *)
+
+fun inst_tab_term (inst, tinst) = if Symtab.is_empty inst
+      then tinst_tab_term tinst
+      else (* instantiate terms and types simultaneously *)
+        let
+          fun instf (Const (x, T)) = Const (x, tinst_tab_type tinst T)
+            | instf (Free (x, T)) = (case Symtab.lookup (inst, x) of
+                 NONE => Free (x, tinst_tab_type tinst T)
+               | SOME t => t)
+            | instf (Var (xi, T)) = Var (xi, tinst_tab_type tinst T)
+            | instf (b as Bound _) = b
+            | instf (Abs (x, T, t)) = Abs (x, tinst_tab_type tinst T, instf t)
+            | instf (s $ t) = instf s $ instf t
+        in instf end;
+
+fun inst_tab_thm sg (inst, tinst) thm = if Symtab.is_empty inst
+      then tinst_tab_thm sg tinst thm
+      else let
+          val cert = Thm.cterm_of sg;
+          val certT = Thm.ctyp_of sg;
+          val {hyps, prop, ...} = Thm.rep_thm thm;
+          (* type instantiations *)
+          val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
+          val tinst' = Symtab.dest tinst |>
+                List.filter (fn (a, _) => a mem_string tfrees);
+          (* term instantiations;
+             note: lhss are type instantiated, because
+                   type insts will be done first*)
+          val frees = foldr Term.add_term_frees [] (prop :: hyps);
+          val inst' = Symtab.dest inst |>
+                List.mapPartial (fn (a, t) =>
+                  get_first (fn (Free (x, T)) => 
+                    if a = x then SOME (Free (x, tinst_tab_type tinst T), t)
+                    else NONE) frees);
+        in
+          if null tinst' andalso null inst' then tinst_tab_thm sg tinst thm
+          else thm |> Drule.implies_intr_list (map cert hyps)
+            |> Drule.tvars_intr_list (map #1 tinst')
+            |> (fn (th, al) => th |> Thm.instantiate
+                ((map (fn (a, T) => (valOf (assoc (al, a)), certT T)) tinst'),
+                  []))
+            |> Drule.forall_intr_list (map (cert o #1) inst')
+            |> Drule.forall_elim_list (map (cert o #2) inst') 
+            |> (fn th => Drule.implies_elim_list th
+                 (map (Thm.assume o cert o inst_tab_term (inst, tinst)) hyps))
+        end;
+
+fun inst_tab_elem _ (_, tinst) (Fixes fixes) =
+      Fixes (map (fn (x, T, mx) => (x, Option.map (tinst_tab_type tinst) T, mx)) fixes)
+  | inst_tab_elem _ inst (Assumes asms) =
+      Assumes (map (apsnd (map (fn (t, (ps, qs)) =>
+        (inst_tab_term inst t,
+          (map (inst_tab_term inst) ps, map (inst_tab_term inst) qs))))) asms)
+  | inst_tab_elem _ inst (Defines defs) =
+      Defines (map (apsnd (fn (t, ps) =>
+        (inst_tab_term inst t, map (inst_tab_term inst) ps))) defs)
+  | inst_tab_elem sg inst (Notes facts) =
+      Notes (map (apsnd (map (apfst (map (inst_tab_thm sg inst))))) facts);
+
+fun inst_tab_elems sign inst ((n, ps), elems) =
+      ((n, map (inst_tab_term inst) ps), map (inst_tab_elem sign inst) elems);
+
 
 (** structured contexts: rename + merge + implicit type instantiation **)
 
@@ -781,7 +917,14 @@
   let val ((ctxt', _), res) =
     foldl_map (activate_elem (name = "")) ((ProofContext.qualified true ctxt, axs), elems)
       handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]
-  in (ProofContext.restore_qualified ctxt ctxt', res) end;
+    val ctxt'' = if name = "" then ctxt'
+          else let
+              val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
+              val ctxt'' = put_local_registration (name, ps') ("", []) ctxt'
+            in foldl (fn (ax, ctxt) =>
+              add_local_witness (name, ps') (Thm.assume (Thm.cprop_of ax)) ctxt) ctxt'' axs
+            end
+  in (ProofContext.restore_qualified ctxt ctxt'', res) end;
 
 fun activate_elemss prep_facts = foldl_map (fn (ctxt, (((name, ps), axs), raw_elems)) =>
   let
@@ -808,6 +951,20 @@
 end;
 
 
+(* register elements *)
+
+fun register_elems (((_, ps), (((name, ax_ps), axs), _)), ctxt) =
+  if name = "" then ctxt
+      else let val ps' = map (fn (n, SOME T) => Free (n, T)) ax_ps
+          val ctxt' = put_local_registration (name, ps') ("", []) ctxt
+        in foldl (fn (ax, ctxt) =>
+          add_local_witness (name, ps') ax ctxt) ctxt' axs
+        end;
+
+fun register_elemss id_elemss ctxt = 
+  foldl register_elems ctxt id_elemss;
+
+
 (** prepare context elements **)
 
 (* expressions *)
@@ -856,8 +1013,8 @@
 *)
 
 fun flatten _ (ids, Elem (Fixes fixes)) =
-      (ids, [((("", map (rpair NONE o #1) fixes), []), Ext (Fixes fixes))])
-  | flatten _ (ids, Elem elem) = (ids, [((("", []), []), Ext elem)])
+      (ids @ [(("", map #1 fixes), ([], []))], [((("", map (rpair NONE o #1) fixes), []), Ext (Fixes fixes))])
+  | flatten _ (ids, Elem elem) = (ids @ [(("", []), ([], []))], [((("", []), []), Ext elem)])
   | flatten (ctxt, prep_expr) (ids, Expr expr) =
       apsnd (map (apsnd Int)) (flatten_expr ctxt (ids, prep_expr expr));
 
@@ -1036,7 +1193,6 @@
     (* CB: process patterns (conclusion and external elements only) *)
     val (ctxt, all_propp) =
       prepp (ProofContext.declare_terms (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
-    
     (* CB: add type information from conclusion and external elements
        to context *)
     val ctxt = ProofContext.declare_terms (List.concat (map (map fst) all_propp)) ctxt;
@@ -1128,14 +1284,21 @@
 
     val (import_ids, raw_import_elemss) = flatten (context, prep_expr sign) ([], Expr import);
     (* CB: normalise "includes" among elements *)
-    val raw_elemss = List.concat (#2 ((foldl_map (flatten (context, prep_expr sign))
-      (import_ids, elements))));
+    val (ids, raw_elemsss) = foldl_map (flatten (context, prep_expr sign))
+      (import_ids, elements);
+
+    val raw_elemss = List.concat raw_elemsss;
     (* CB: raw_import_elemss @ raw_elemss is the normalised list of
        context elements obtained from import and elements. *)
     val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
       context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
+    (* replace extended ids (for axioms) by ids *)
+    val all_elemss' = map (fn (((_, ps), _), (((n, ps'), ax), elems)) =>
+        (((n, List.filter (fn (p, _) => p mem ps) ps'), ax), elems))
+      (ids ~~ all_elemss);
+
     (* CB: all_elemss and parms contain the correct parameter types *)
-    val (ps,qs) = splitAt(length raw_import_elemss, all_elemss)
+    val (ps,qs) = splitAt(length raw_import_elemss, all_elemss')
     val (import_ctxt, (import_elemss, _)) =
       activate_facts prep_facts (context, ps);
 
@@ -1162,7 +1325,7 @@
           let val {predicate = (stmt, _), params = (ps, _), ...} =
             the_locale thy name
           in (stmt, param_types ps, Locale name) end);
-    val ((((locale_ctxt, _), (elems_ctxt, _)), _), (elems_stmt, concl')) =
+    val ((((locale_ctxt, locale_elemss), (elems_ctxt, _)), _), (elems_stmt, concl')) =
       prep_ctxt false fixed_params import elems concl ctxt;
   in (locale, (target_stmt, elems_stmt), locale_ctxt, elems_ctxt, concl') end;
 
@@ -1404,6 +1567,8 @@
 
 in
 
+(* store exported theorem in theory *)
+
 fun note_thmss_qualified kind name args thy =
   thy
   |> Theory.add_path (Sign.base_name name)
@@ -1411,30 +1576,84 @@
   |>> hide_bound_names (map (#1 o #1) args)
   |>> Theory.parent_path;
 
-fun note_thms_qualified' kind (arg as ((name, atts), thms)) thy =
+(* accesses of interpreted theorems *)
+
+(* fully qualified name in theory is T.p.r.n where
+   T: theory name, p: interpretation prefix, r: renaming prefix, n: name *)
+
+fun global_accesses prfx name =
+     if prfx = "" then
+       case NameSpace.unpack name of
+	   [] => [""]
+	 | [T, n] => map NameSpace.pack [[T, n], [n]]
+	 | [T, r, n] => map NameSpace.pack [[T, r, n], [T, n], [r, n], [n]]
+	 | _ => error ("Locale accesses: illegal name " ^ quote name)
+     else case NameSpace.unpack name of
+           [] => [""]
+         | [T, p, n] => map NameSpace.pack [[T, p, n], [p, n]]
+         | [T, p, r, n] => map NameSpace.pack
+             [[T, p, r, n], [T, p, n], [p, r, n], [p, n]]
+         | _ => error ("Locale accesses: illegal name " ^ quote name);
+
+(* fully qualified name in context is p.r.n where
+   p: interpretation prefix, r: renaming prefix, n: name *)
+
+fun local_accesses prfx name =
+     if prfx = "" then
+       case NameSpace.unpack name of
+	   [] => [""]
+	 | [n] => map NameSpace.pack [[n]]
+	 | [r, n] => map NameSpace.pack [[r, n], [n]]
+	 | _ => error ("Locale accesses: illegal name " ^ quote name)
+     else case NameSpace.unpack name of
+           [] => [""]
+         | [p, n] => map NameSpace.pack [[p, n]]
+         | [p, r, n] => map NameSpace.pack [[p, r, n], [p, n]]
+         | _ => error ("Locale accesses: illegal name " ^ quote name);
+
+
+(* store instantiations of args for all registered interpretations
+   of the theory *)
+
+fun note_thmss_registrations kind target args thy =
   let
-    val qname = NameSpace.unpack name
-  in
-    if length qname <= 1
-    then PureThy.note_thmss_i kind [arg] thy
-  else let val (prfx, n) = split_last qname
-    in thy
-      |> Theory.add_path (NameSpace.pack prfx)
-      |> PureThy.note_thmss_i kind [((n, atts), thms)]
-      |>> funpow (length prfx) Theory.parent_path
-    end
-  end;
+    val ctxt = ProofContext.init thy;
+    val sign = Theory.sign_of thy;
+
+    val (parms, parmTs_o) =
+          the_locale thy target |> #params |> fst |> split_list;
+    val parmvTs = map (Type.varifyT o valOf) parmTs_o;
+    val ids = flatten (ctxt, intern_expr sign) ([], Expr (Locale target))
+          |> fst |> map fst;
+
+    val regs = get_global_registrations thy target;
+
+    (* add args to thy for all registrations *)
 
-(* prfx may be empty (not yet), names (in args) may be qualified *)
+    fun activate (thy, (vts, ((prfx, atts2), _))) =
+      let
+        val ts = map Logic.unvarify vts;
+        (* type instantiation *)
+        val vtinst = Library.foldl (Type.typ_match (Sign.tsig_of sign))
+             (Vartab.empty, (parmvTs ~~ map Term.fastype_of ts));
+        val tinst = Vartab.dest vtinst |> map (fn ((x, 0), T) => (x, T))
+             |> Symtab.make;            
+        (* replace parameter names in ids by instantiations *)
+        val vinst = Symtab.make (parms ~~ vts);
+        fun vinst_names ps = map (fn p => Symtab.lookup (vinst, p) |> valOf) ps;
+        val inst = Symtab.make (parms ~~ ts);
+        val ids' = map (apsnd vinst_names) ids;
+        val prems = List.concat (map (snd o valOf o get_global_registration thy) ids');
+        val args' = map (fn ((n, atts), [(ths, [])]) =>
+            ((if prfx = "" orelse n = "" then ""
+              else NameSpace.pack [prfx, n], map fst atts @ atts2),
+             [(map (Drule.standard o Drule.satisfy_hyps prems o inst_tab_thm sign (inst, tinst)) ths, [])]))
+          args;
+      in
+        PureThy.note_thmss_accesses_i (global_accesses prfx) (Drule.kind kind) args' thy |> fst
+      end;
+  in Library.foldl activate (thy, regs) end;
 
-fun note_thmss_qualified' kind prfx args thy =
-  thy
-  |> Theory.add_path (Sign.base_name prfx)
-  |> (fn thy => Library.foldl (fn ((thy, res), arg) =>
-        let val (thy', res') = note_thms_qualified' (Drule.kind kind) arg thy
-        in (thy', res @ res') end) ((thy, []), args))
-(*  |>> hide_bound_names (map (#1 o #1) args) *)
-  |>> Theory.parent_path;
 
 fun smart_note_thmss kind NONE = PureThy.note_thmss_i (Drule.kind kind)
   | smart_note_thmss kind (SOME (loc, _)) = note_thmss_qualified kind loc;
@@ -1444,6 +1663,8 @@
 
 local
 
+(* add facts to locale in theory *)
+
 fun put_facts loc args thy =
   let
     val {predicate, import, elems, params} = the_locale thy loc;
@@ -1452,6 +1673,9 @@
   in thy |> put_locale loc {predicate = predicate, import = import, elems = elems @ [(note, stamp ())],
     params = params} end;
 
+(* add theorem to locale and theory,
+   base for theorems (in loc) and declare (in loc) *)
+
 fun gen_note_thmss prep_locale get_thms kind raw_loc raw_args thy =
   let
     val thy_ctxt = ProofContext.init thy;
@@ -1470,6 +1694,7 @@
   in
     thy
     |> put_facts loc args
+    |> note_thmss_registrations kind loc args
     |> note_thmss_qualified kind loc args'
   end;
 
@@ -1483,13 +1708,14 @@
 
 (* CB: only used in Proof.finish_global. *)
 
-fun add_thmss loc args (thy, ctxt) =
+fun add_thmss kind loc args (thy, ctxt) =
   let
     val args' = map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])) args;
     val thy' = put_facts loc args' thy;
+    val thy'' = note_thmss_registrations kind loc args' thy';
     val (ctxt', (_, facts')) =
       activate_facts (K I) (ctxt, [((("", []), []), [Notes args'])]);
-  in ((thy', ctxt'), facts') end;
+  in ((thy'', ctxt'), facts') end;
 
 end;
 
@@ -1688,112 +1914,6 @@
 
 (** instantiate free vars **)
 
-(* instantiate TFrees *)
-
-fun tinst_type tinst T = if Symtab.is_empty tinst
-      then T
-      else Term.map_type_tfree
-        (fn (v as (x, _)) => getOpt (Symtab.lookup (tinst, x), (TFree v))) T;
-
-fun tinst_term tinst t = if Symtab.is_empty tinst
-      then t
-      else Term.map_term_types (tinst_type tinst) t;
-
-fun tinst_thm sg tinst thm = if Symtab.is_empty tinst
-      then thm
-      else let
-          val cert = Thm.cterm_of sg;
-          val certT = Thm.ctyp_of sg;
-          val {hyps, prop, ...} = Thm.rep_thm thm;
-          val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
-          val tinst' = Symtab.dest tinst |>
-                List.filter (fn (a, _) => a mem_string tfrees);
-        in
-          if null tinst' then thm
-          else thm |> Drule.implies_intr_list (map cert hyps)
-            |> Drule.tvars_intr_list (map #1 tinst')
-            |> (fn (th, al) => th |> Thm.instantiate
-                ((map (fn (a, T) => (valOf (assoc (al, a)), certT T)) tinst'),
-                  []))
-            |> (fn th => Drule.implies_elim_list th
-                 (map (Thm.assume o cert o tinst_term tinst) hyps))
-        end;
-
-fun tinst_elem _ tinst (Fixes fixes) =
-      Fixes (map (fn (x, T, mx) => (x, Option.map (tinst_type tinst) T, mx)) fixes)
-  | tinst_elem _ tinst (Assumes asms) =
-      Assumes (map (apsnd (map (fn (t, (ps, qs)) =>
-        (tinst_term tinst t,
-          (map (tinst_term tinst) ps, map (tinst_term tinst) qs))))) asms)
-  | tinst_elem _ tinst (Defines defs) =
-      Defines (map (apsnd (fn (t, ps) =>
-        (tinst_term tinst t, map (tinst_term tinst) ps))) defs)
-  | tinst_elem sg tinst (Notes facts) =
-      Notes (map (apsnd (map (apfst (map (tinst_thm sg tinst))))) facts);
-
-(* instantiate TFrees and Frees *)
-
-fun inst_term (inst, tinst) = if Symtab.is_empty inst
-      then tinst_term tinst
-      else (* instantiate terms and types simultaneously *)
-        let
-          fun instf (Const (x, T)) = Const (x, tinst_type tinst T)
-            | instf (Free (x, T)) = (case Symtab.lookup (inst, x) of
-                 NONE => Free (x, tinst_type tinst T)
-               | SOME t => t)
-            | instf (Var (xi, T)) = Var (xi, tinst_type tinst T)
-            | instf (b as Bound _) = b
-            | instf (Abs (x, T, t)) = Abs (x, tinst_type tinst T, instf t)
-            | instf (s $ t) = instf s $ instf t
-        in instf end;
-
-fun inst_thm sg (inst, tinst) thm = if Symtab.is_empty inst
-      then tinst_thm sg tinst thm
-      else let
-          val cert = Thm.cterm_of sg;
-          val certT = Thm.ctyp_of sg;
-          val {hyps, prop, ...} = Thm.rep_thm thm;
-          (* type instantiations *)
-          val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
-          val tinst' = Symtab.dest tinst |>
-                List.filter (fn (a, _) => a mem_string tfrees);
-          (* term instantiations;
-             note: lhss are type instantiated, because
-                   type insts will be done first*)
-          val frees = foldr Term.add_term_frees [] (prop :: hyps);
-          val inst' = Symtab.dest inst |>
-                List.mapPartial (fn (a, t) =>
-                  get_first (fn (Free (x, T)) => 
-                    if a = x then SOME (Free (x, tinst_type tinst T), t)
-                    else NONE) frees);
-        in
-          if null tinst' andalso null inst' then tinst_thm sg tinst thm
-          else thm |> Drule.implies_intr_list (map cert hyps)
-            |> Drule.tvars_intr_list (map #1 tinst')
-            |> (fn (th, al) => th |> Thm.instantiate
-                ((map (fn (a, T) => (valOf (assoc (al, a)), certT T)) tinst'),
-                  []))
-            |> Drule.forall_intr_list (map (cert o #1) inst')
-            |> Drule.forall_elim_list (map (cert o #2) inst') 
-            |> (fn th => Drule.implies_elim_list th
-                 (map (Thm.assume o cert o inst_term (inst, tinst)) hyps))
-        end;
-
-fun inst_elem _ (_, tinst) (Fixes fixes) =
-      Fixes (map (fn (x, T, mx) => (x, Option.map (tinst_type tinst) T, mx)) fixes)
-  | inst_elem _ inst (Assumes asms) =
-      Assumes (map (apsnd (map (fn (t, (ps, qs)) =>
-        (inst_term inst t,
-          (map (inst_term inst) ps, map (inst_term inst) qs))))) asms)
-  | inst_elem _ inst (Defines defs) =
-      Defines (map (apsnd (fn (t, ps) =>
-        (inst_term inst t, map (inst_term inst) ps))) defs)
-  | inst_elem sg inst (Notes facts) =
-      Notes (map (apsnd (map (apfst (map (inst_thm sg inst))))) facts);
-
-fun inst_elems sign inst ((n, ps), elems) =
-      ((n, map (inst_term inst) ps), map (inst_elem sign inst) elems);
-
 (* extract proof obligations (assms and defs) from elements *)
 
 (* check if defining equation has become t == t, these are dropped
@@ -1829,9 +1949,9 @@
       let
         (* extract theory or context attributes *)
         val (Notes facts) = map_attrib_element_i which (Notes facts);
-        (* add attributs from registration *)
+        (* add attributes from registration *)
         val facts' = map (apfst (apsnd (fn a => a @ atts))) facts;
-        (* discharge hyps and varify *)
+        (* discharge hyps  *)
         val facts'' = map (apsnd (map (apfst (map disch)))) facts';
         (* prefix names *)
         val facts''' = map (apfst (apfst (fn name =>
@@ -1862,55 +1982,36 @@
       in Library.foldl (activate_facts_elems get_reg note_thmss which
         (standard o Drule.satisfy_hyps prems)) (thy_ctxt, new_elemss) end;
 
-fun loc_accesses prfx name =
-  (* full qualified name is T.p.r.n where
-       T: theory name, p: interpretation prefix, r: renaming prefix, n: name
-  *)
-     if prfx = "" then
-       case NameSpace.unpack name of
-	   [] => [""]
-	 | [T, n] => map NameSpace.pack [[T, n], [n]]
-	 | [T, r, n] => map NameSpace.pack [[T, r, n], (*[T, n],*) [r, n], [n]]
-	 | _ => error ("Locale accesses: illegal name " ^ quote name)
-     else case NameSpace.unpack name of
-           [] => [""]
-         | [T, p, n] => map NameSpace.pack [[T, p, n], [p, n]]
-         | [T, p, r, n] => map NameSpace.pack
-             [[T, p, r, n], [T, p, n], [p, r, n], [p, n]]
-         | _ => error ("Locale accesses: illegal name " ^ quote name);
-
 val global_activate_facts_elemss = gen_activate_facts_elemss
-      get_global_registration
-      (fn prfx => PureThy.note_thmss_qualified_i (loc_accesses prfx)
+      (fn thy => fn (name, ps) =>
+        get_global_registration thy (name, map Logic.varify ps))
+      (fn prfx => PureThy.note_thmss_accesses_i (global_accesses prfx)
         (Drule.kind ""))
       fst Drule.standard;
 val local_activate_facts_elemss = gen_activate_facts_elemss
-      get_local_registration (fn prfx => fn _ => fn ctxt => (ctxt, ctxt)) snd I;
-(*
-val local_activate_facts_elemss = gen_activate_facts_elemss
-      get_local_registration (fn prfx => ProofContext.note_thmss_i) snd I;
-*)
+      get_local_registration
+      (fn prfx => ProofContext.note_thmss_accesses_i (local_accesses prfx))
+      snd I;
 
-fun gen_prep_registration mk_ctxt read_terms test_reg put_reg activate
+fun gen_prep_registration mk_ctxt is_local read_terms test_reg put_reg activate
     attn expr insts thy_ctxt =
   let
     val ctxt = mk_ctxt thy_ctxt;
     val sign = ProofContext.sign_of ctxt;
 
-    val (ids, raw_elemss) =
-          flatten (ctxt, intern_expr sign) ([], Expr expr);
+    val ctxt' = ctxt |> ProofContext.theory_of |> ProofContext.init;
+    val (ids, raw_elemss) = flatten (ctxt', intern_expr sign) ([], Expr expr);
     val do_close = false;  (* effect unknown *)
     val ((parms, all_elemss, _), (spec, (xs, defs, _))) =
-          read_elemss do_close ctxt [] raw_elemss [];
+          read_elemss do_close ctxt' [] raw_elemss [];
 
 
     (** compute instantiation **)
 
-    (* check user input *)
+    (* user input *)
     val insts = if length parms < length insts
          then error "More arguments than parameters in instantiation."
          else insts @ replicate (length parms - length insts) NONE;
-
     val (ps, pTs) = split_list parms;
     val pvTs = map Type.varifyT pTs;
 
@@ -1922,17 +2023,26 @@
     val used = foldr Term.add_typ_varnames [] pvTs;
     fun sorts (a, i) = assoc (tvars, (a, i));
     val (vs, vinst) = read_terms thy_ctxt sorts used given_insts;
+    val vars = foldl Term.add_term_tvar_ixns [] vs \\ map fst tvars;
+    val vars' = Library.foldl Term.add_term_varnames (vars, vs);
+    val _ = if null vars' then ()
+         else error ("Illegal schematic variable(s) in instantiation: " ^
+           commas_quote (map Syntax.string_of_vname vars'));
     (* replace new types (which are TFrees) by ones with new names *)
     val new_Tnames = foldr Term.add_term_tfree_names [] vs;
     val new_Tnames' = Term.invent_names used "'a" (length new_Tnames);
-    val renameT = Term.map_type_tfree (fn (a, s) =>
-          TFree (valOf (assoc (new_Tnames ~~ new_Tnames', a)), s));
-    val rename = Term.map_term_types renameT;
+    val renameT =
+          if is_local then I
+          else Type.unvarifyT o Term.map_type_tfree (fn (a, s) =>
+            TFree (valOf (assoc (new_Tnames ~~ new_Tnames', a)), s));
+    val rename =
+          if is_local then I
+          else Term.map_term_types renameT;
 
     val tinst = Symtab.make (map
-                (fn ((x, 0), T) => (x, T |> renameT |> Type.unvarifyT)
-                  | ((_, n), _) => error "Var in prep_registration") vinst);
-    val inst = Symtab.make (given_ps ~~ map (Logic.unvarify o rename) vs);
+                (fn ((x, 0), T) => (x, T |> renameT)
+                  | ((_, n), _) => error "Internal error var in prep_registration") vinst);
+    val inst = Symtab.make (given_ps ~~ map rename vs);
 
     (* defined params without user input *)
     val not_given = List.mapPartial (fn (x, (NONE, T)) => SOME (x, T)
@@ -1942,10 +2052,10 @@
         val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of
                NONE => error ("Instance missing for parameter " ^ quote p)
              | SOME (Free (_, T), t) => (t, T);
-        val d = t |> inst_term (inst, tinst) |> Envir.beta_norm;
+        val d = t |> inst_tab_term (inst, tinst) |> Envir.beta_norm;
       in (Symtab.update_new ((p, d), inst), tinst) end;
     val (inst, tinst) = Library.foldl add_def ((inst, tinst), not_given);
-  
+    (* Note: inst and tinst contain no vars. *)
 
     (** compute proof obligations **)
 
@@ -1955,7 +2065,7 @@
 
     (* instantiate ids and elements *)
     val inst_elemss = map
-          (fn (id, (_, elems)) => inst_elems sign (inst, tinst) (id, 
+          (fn (id, (_, elems)) => inst_tab_elems sign (inst, tinst) (id, 
             map (fn Int e => e) elems)) 
           (ids' ~~ all_elemss);
 
@@ -1966,8 +2076,11 @@
     val propss = extract_asms_elemss new_inst_elemss;
 
 
-    (** add registrations to theory,
+    (** add registrations to theory or context,
         without theorems, these are added after the proof **)
+    (* TODO: this is potentially problematic, since a proof of the
+       interpretation might contain a reference to the incomplete
+       registration. *)
 
     val thy_ctxt' = Library.foldl (fn (thy_ctxt, (id, _)) =>
           put_reg id attn thy_ctxt) (thy_ctxt, new_inst_elemss);
@@ -1977,15 +2090,16 @@
 in
 
 val prep_global_registration = gen_prep_registration
-     ProofContext.init
+     ProofContext.init false
      (fn thy => fn sorts => fn used =>
        Sign.read_def_terms (Theory.sign_of thy, K NONE, sorts) used true)
-     test_global_registration
-     put_global_registration
+     (fn thy => fn (name, ps) =>
+       test_global_registration thy (name, map Logic.varify ps))
+     (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
      global_activate_facts_elemss;
 
 val prep_local_registration = gen_prep_registration
-     I
+     I true
      (fn ctxt => ProofContext.read_termTs ctxt (K false) (K NONE))
      smart_test_registration
      put_local_registration

--- a/src/Pure/Isar/proof.ML	Mon Apr 11 12:18:27 2005 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Apr 11 12:34:34 2005 +0200
@@ -90,13 +90,17 @@
   val def: string -> context attribute list -> string *  (string * string list) -> state -> state
   val def_i: string -> context attribute list -> string * (term * term list) -> state -> state
   val invoke_case: string * string option list * context attribute list -> state -> state
-  val multi_theorem: string -> (theory -> theory)
-    -> (xstring * (Locale.multi_attribute list * Locale.multi_attribute list list)) option
+  val multi_theorem:
+    string -> (theory -> theory) ->
+    (cterm list -> context -> context -> thm -> thm) ->
+    (xstring * (Locale.multi_attribute list * Locale.multi_attribute list list)) option
     -> bstring * theory attribute list -> Locale.multi_attribute Locale.element Locale.elem_expr list
     -> ((bstring * theory attribute list) * (string * (string list * string list)) list) list
     -> theory -> state
-  val multi_theorem_i: string -> (theory -> theory)
-    -> (string * (Locale.multi_attribute list * Locale.multi_attribute list list)) option
+  val multi_theorem_i:
+    string -> (theory -> theory)  ->
+    (cterm list -> context -> context -> thm -> thm) ->
+    (string * (Locale.multi_attribute list * Locale.multi_attribute list list)) option
     -> bstring * theory attribute list
     -> Locale.multi_attribute Locale.element_i Locale.elem_expr list
     -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
@@ -162,10 +166,12 @@
     theory_spec: (bstring * theory attribute list) * theory attribute list list,
     locale_spec: (string * (Locale.multi_attribute list * Locale.multi_attribute list list)) option,
     view: cterm list * cterm list, (* target view and includes view *)
-    thy_mod: theory -> theory} |   (* used in finish_global to modify final
+    thy_mod: theory -> theory,     (* used in finish_global to modify final
                                       theory, normally set to I; used by
                                       registration command to activate
                                       registrations *)
+    export: cterm list -> context -> context -> thm -> thm } |
+                                   (* exporter to be used in finish_global *)
   Show of context attribute list list |
   Have of context attribute list list |
   Interpret of {attss: context attribute list list,
@@ -796,7 +802,7 @@
   end;
 
 (*global goals*)
-fun global_goal prep kind thy_mod raw_locale a elems concl thy =
+fun global_goal prep kind thy_mod export raw_locale a elems concl thy =
   let
     val init = init_state thy;
     val (opt_name, view, locale_ctxt, elems_ctxt, propp) =
@@ -814,7 +820,8 @@
         theory_spec = (a, map (snd o fst) concl),
         locale_spec = (case raw_locale of NONE => NONE | SOME (_, x) => SOME (valOf opt_name, x)),
         view = view,
-        thy_mod = thy_mod})
+        thy_mod = thy_mod,
+        export = export})
       Seq.single true (map (fst o fst) concl) propp
   end;
 
@@ -927,27 +934,28 @@
     val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), _)) = current_goal state;
     val locale_ctxt = context_of (state |> close_block);
     val theory_ctxt = context_of (state |> close_block |> close_block);
-    val {kind = k, theory_spec = ((name, atts), attss), locale_spec, view = (target_view, elems_view), thy_mod} =
+    val {kind = k, theory_spec = ((name, atts), attss), locale_spec, view = (target_view, elems_view), thy_mod, export} =
       (case kind of Theorem x => x | _ => err_malformed "finish_global" state);
 
     val ts = List.concat tss;
-    val locale_results = map (ProofContext.export_standard elems_view goal_ctxt locale_ctxt)
+    val locale_results = map (export elems_view goal_ctxt locale_ctxt)
       (prep_result state ts raw_thm);
 
     val results = map (Drule.strip_shyps_warning o
-      ProofContext.export_standard target_view locale_ctxt theory_ctxt) locale_results;
+      export target_view locale_ctxt theory_ctxt) locale_results;
 
     val (theory', results') =
       theory_of state
-      |> (case locale_spec of NONE => I | SOME (loc, (loc_atts, loc_attss)) => fn thy =>
+      |> (case locale_spec of NONE => I
+                            | SOME (loc, (loc_atts, loc_attss)) => fn thy =>
         if length names <> length loc_attss then
           raise THEORY ("Bad number of locale attributes", [thy])
         else (thy, locale_ctxt)
-          |> Locale.add_thmss loc ((names ~~ Library.unflat tss locale_results) ~~ loc_attss)
+          |> Locale.add_thmss k loc ((names ~~ Library.unflat tss locale_results) ~~ loc_attss)
           |> (fn ((thy', ctxt'), res) =>
             if name = "" andalso null loc_atts then thy'
             else (thy', ctxt')
-              |> (#1 o #1 o Locale.add_thmss loc [((name, List.concat (map #2 res)), loc_atts)])))
+              |> (#1 o #1 o Locale.add_thmss k loc [((name, List.concat (map #2 res)), loc_atts)])))
       |> Locale.smart_note_thmss k locale_spec
         ((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results))
       |> (fn (thy, res) => (thy, res)

--- a/src/Pure/Isar/proof_context.ML	Mon Apr 11 12:18:27 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Apr 11 12:34:34 2005 +0200
@@ -67,6 +67,7 @@
   val find_free: term -> string -> term option
   val export: bool -> context -> context -> thm -> thm Seq.seq
   val export_standard: cterm list -> context -> context -> thm -> thm
+  val export_plain: cterm list -> context -> context -> thm -> thm
   val drop_schematic: indexname * term option -> indexname * term option
   val add_binds: (indexname * string option) list -> context -> context
   val add_binds_i: (indexname * term option) list -> context -> context
@@ -103,11 +104,23 @@
   val put_thmss: (string * thm list) list -> context -> context
   val reset_thms: string -> context -> context
   val note_thmss:
-    ((bstring * context attribute list) * (thmref * context attribute list) list) list ->
-      context -> context * (bstring * thm list) list
+    ((bstring * context attribute list) *
+      (thmref * context attribute list) list) list ->
+    context -> context * (bstring * thm list) list
   val note_thmss_i:
-    ((bstring * context attribute list) * (thm list * context attribute list) list) list ->
-      context -> context * (bstring * thm list) list
+    ((bstring * context attribute list) *
+      (thm list * context attribute list) list) list ->
+    context -> context * (bstring * thm list) list
+  val note_thmss_accesses:
+    (string -> string list) ->
+    ((bstring * context attribute list) *
+      (thmref * context attribute list) list) list ->
+    context -> context * (bstring * thm list) list
+  val note_thmss_accesses_i:
+    (string -> string list) ->
+    ((bstring * context attribute list) *
+      (thm list * context attribute list) list) list ->
+    context -> context * (bstring * thm list) list
   val export_assume: exporter
   val export_presume: exporter
   val cert_def: context -> term -> string * term
@@ -812,16 +825,31 @@
       end)
   end;
 
+(* without varification *)
+
+fun export_view' view is_goal inner outer =
+  let
+    val asms = Library.drop (length (assumptions_of outer), assumptions_of inner);
+    val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms;
+  in fn thm =>thm
+    |> Tactic.norm_hhf_plain
+    |> Seq.EVERY (rev exp_asms)
+    |> Seq.map (Drule.implies_intr_list view)
+    |> Seq.map Tactic.norm_hhf_plain
+  end;
+
 val export = export_view [];
 
-fun export_standard view inner outer =
-  let val exp = export_view view false inner outer in
+fun gen_export_std exp_view view inner outer =
+  let val exp = exp_view view false inner outer in
     fn th =>
       (case Seq.pull (exp th) of
         SOME (th', _) => th' |> Drule.local_standard
       | NONE => raise CONTEXT ("Internal failure while exporting theorem", inner))
   end;
 
+val export_standard = gen_export_std export_view;
+val export_plain = gen_export_std export_view';
 
 
 (** bindings **)
@@ -1022,20 +1050,24 @@
 
 (* put_thm(s) *)
 
-fun put_thms ("", _) ctxt = ctxt
-  | put_thms (name, ths) ctxt = ctxt |> map_context
+fun gen_put_thms _ _ ("", _) ctxt = ctxt
+  | gen_put_thms override_q acc (name, ths) ctxt = ctxt |> map_context
       (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count) =>
-        if not q andalso NameSpace.is_qualified name then
+        if not override_q andalso not q andalso NameSpace.is_qualified name then
           raise CONTEXT ("Attempt to declare qualified name " ^ quote name, ctxt)
-        else (thy, syntax, data, asms, binds, (q, NameSpace.extend (space, [name]),
+        else (thy, syntax, data, asms, binds, (q, NameSpace.extend' acc (space, [name]),
           Symtab.update ((name, SOME ths), tab),
             FactIndex.add (is_known ctxt) (index, (name, ths))), cases, defs, delta, delta_count));
 
-fun put_thm (name, th) = put_thms (name, [th]);
+fun gen_put_thm q acc (name, th) = gen_put_thms q acc (name, [th]);
 
-fun put_thmss [] ctxt = ctxt
-  | put_thmss (th :: ths) ctxt = ctxt |> put_thms th |> put_thmss ths;
+fun gen_put_thmss q acc [] ctxt = ctxt
+  | gen_put_thmss q acc (th :: ths) ctxt =
+      ctxt |> gen_put_thms q acc th |> gen_put_thmss q acc ths;
 
+val put_thm = gen_put_thm false NameSpace.accesses;
+val put_thms = gen_put_thms false NameSpace.accesses;
+val put_thmss = gen_put_thmss false NameSpace.accesses;
 
 (* reset_thms *)
 
@@ -1049,21 +1081,25 @@
 
 local
 
-fun gen_note_thss get (ctxt, ((name, more_attrs), ths_attrs)) =
+fun gen_note_thss get acc (ctxt, ((name, more_attrs), ths_attrs)) =
   let
     fun app ((ct, ths), (th, attrs)) =
       let val (ct', th') = Thm.applys_attributes ((ct, get ctxt th), attrs @ more_attrs)
       in (ct', th' :: ths) end;
     val (ctxt', rev_thms) = Library.foldl app ((ctxt, []), ths_attrs);
     val thms = List.concat (rev rev_thms);
-  in (ctxt' |> put_thms (name, thms), (name, thms)) end;
+  in (ctxt' |> gen_put_thms true acc (name, thms), (name, thms)) end;
 
-fun gen_note_thmss get args ctxt = foldl_map (gen_note_thss get) (ctxt, args);
+fun gen_note_thmss get acc args ctxt =
+  foldl_map (gen_note_thss get acc) (ctxt, args);
 
 in
 
-val note_thmss = gen_note_thmss get_thms;
-val note_thmss_i = gen_note_thmss (K I);
+val note_thmss = gen_note_thmss get_thms NameSpace.accesses;
+val note_thmss_i = gen_note_thmss (K I) NameSpace.accesses;
+
+val note_thmss_accesses = gen_note_thmss get_thms;
+val note_thmss_accesses_i = gen_note_thmss (K I);
 
 end;
 

--- a/src/Pure/axclass.ML	Mon Apr 11 12:18:27 2005 +0200
+++ b/src/Pure/axclass.ML	Mon Apr 11 12:34:34 2005 +0200
@@ -407,7 +407,7 @@
 
 fun inst_proof mk_prop add_thms inst int theory =
   theory
-  |> IsarThy.multi_theorem_i Drule.internalK I
+  |> IsarThy.multi_theorem_i Drule.internalK I ProofContext.export_standard
     ("", [fn (thy, th) => (add_thms [th] thy, th)]) []
     (map (fn t => (("", []), [(t, ([], []))])) (mk_prop (Theory.sign_of theory) inst)) int;
 

--- a/src/Pure/library.ML	Mon Apr 11 12:18:27 2005 +0200
+++ b/src/Pure/library.ML	Mon Apr 11 12:34:34 2005 +0200
@@ -128,6 +128,7 @@
   val radixstring: int * string * int -> string
   val string_of_int: int -> string
   val string_of_indexname: string * int -> string
+    (* CB: note alternative Syntax.string_of_vname has nicer syntax *)
   val read_radixint: int * string list -> int * string list
   val read_int: string list -> int * string list
   val oct_char: string -> string

--- a/src/Pure/pure_thy.ML	Mon Apr 11 12:18:27 2005 +0200
+++ b/src/Pure/pure_thy.ML	Mon Apr 11 12:34:34 2005 +0200
@@ -53,12 +53,12 @@
     theory attribute -> ((bstring * theory attribute list) *
     (thm list * theory attribute list) list) list -> theory ->
     theory * (bstring * thm list) list
-  val note_thmss_qualified:
+  val note_thmss_accesses:
     (string -> string list) ->
     theory attribute -> ((bstring * theory attribute list) *
     (thmref * theory attribute list) list) list -> theory ->
     theory * (bstring * thm list) list
-  val note_thmss_qualified_i:
+  val note_thmss_accesses_i:
     (string -> string list) ->
     theory attribute -> ((bstring * theory attribute list) *
     (thm list * theory attribute list) list) list -> theory ->
@@ -387,9 +387,9 @@
 (* always permit qualified names,
    clients may specify non-standard access policy *)
 
-fun note_thmss_qualified acc =
+fun note_thmss_accesses acc =
   gen_note_thmss (gen_enter_thms Sign.full_name' acc) get_thms;
-fun note_thmss_qualified_i acc =
+fun note_thmss_accesses_i acc =
   gen_note_thmss (gen_enter_thms Sign.full_name' acc) (K I);
 
 end;

--- a/src/Pure/tactic.ML	Mon Apr 11 12:18:27 2005 +0200
+++ b/src/Pure/tactic.ML	Mon Apr 11 12:34:34 2005 +0200
@@ -70,6 +70,7 @@
   val net_biresolve_tac : (bool*thm) list -> int -> tactic
   val net_match_tac     : thm list -> int -> tactic
   val net_resolve_tac   : thm list -> int -> tactic
+  val norm_hhf_plain    : thm -> thm
   val norm_hhf_rule     : thm -> thm
   val norm_hhf_tac      : int -> tactic
   val prune_params_tac  : tactic
@@ -532,9 +533,12 @@
 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
 fun rewtac def = rewrite_goals_tac [def];
 
+fun norm_hhf_plain th =
+  if Drule.is_norm_hhf (prop_of th) then th
+  else rewrite_rule [Drule.norm_hhf_eq] th;
+
 fun norm_hhf_rule th =
- (if Drule.is_norm_hhf (prop_of th) then th
-  else rewrite_rule [Drule.norm_hhf_eq] th) |> Drule.gen_all;
+  th |> norm_hhf_plain |> Drule.gen_all;
 
 val norm_hhf_tac =
   rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)

--- a/src/ZF/Constructible/L_axioms.thy	Mon Apr 11 12:18:27 2005 +0200
+++ b/src/ZF/Constructible/L_axioms.thy	Mon Apr 11 12:34:34 2005 +0200
@@ -100,6 +100,10 @@
   apply (rule L_nat)
   done
 
+interpretation M_trivial ["L"] by (rule M_trivial_L)
+
+(* Replaces the following code.
+
 lemmas rall_abs = M_trivial.rall_abs [OF M_trivial_L]
   and rex_abs = M_trivial.rex_abs [OF M_trivial_L]
   and ball_iff_equiv = M_trivial.ball_iff_equiv [OF M_trivial_L]
@@ -182,7 +186,7 @@
 declare number1_abs [simp]
 declare number2_abs [simp]
 declare number3_abs [simp]
-
+*)
 
 subsection{*Instantiation of the locale @{text reflection}*}