Merged.

--- a/src/FOL/ex/NewLocaleTest.thy	Thu Dec 18 11:16:48 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Fri Dec 19 15:05:37 2008 +0100
@@ -164,6 +164,9 @@
   assumes semi_homh: "semi_hom(prod, sum, h)"
   notes semi_hom_mult = semi_hom_mult [OF semi_homh]
 
+thm semi_hom_loc.semi_hom_mult
+(* unspecified, attribute not applied in backgroud theory !!! *)
+
 lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))"
   by (rule semi_hom_mult)
 

--- a/src/HOL/Algebra/Group.thy	Thu Dec 18 11:16:48 2008 +0100
+++ b/src/HOL/Algebra/Group.thy	Fri Dec 19 15:05:37 2008 +0100
@@ -541,15 +541,6 @@
     {h. h \<in> carrier G -> carrier H &
       (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
 
-lemma hom_mult:
-  "[| h \<in> hom G H; x \<in> carrier G; y \<in> carrier G |]
-   ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
-  by (simp add: hom_def)
-
-lemma hom_closed:
-  "[| h \<in> hom G H; x \<in> carrier G |] ==> h x \<in> carrier H"
-  by (auto simp add: hom_def funcset_mem)
-
 lemma (in group) hom_compose:
      "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
 apply (auto simp add: hom_def funcset_compose) 
@@ -589,8 +580,20 @@
 locale group_hom = G: group G + H: group H for G (structure) and H (structure) +
   fixes h
   assumes homh: "h \<in> hom G H"
-  notes hom_mult [simp] = hom_mult [OF homh]
-    and hom_closed [simp] = hom_closed [OF homh]
+
+lemma (in group_hom) hom_mult [simp]:
+  "[| x \<in> carrier G; y \<in> carrier G |] ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
+proof -
+  assume "x \<in> carrier G" "y \<in> carrier G"
+  with homh [unfolded hom_def] show ?thesis by simp
+qed
+
+lemma (in group_hom) hom_closed [simp]:
+  "x \<in> carrier G ==> h x \<in> carrier H"
+proof -
+  assume "x \<in> carrier G"
+  with homh [unfolded hom_def] show ?thesis by (auto simp add: funcset_mem)
+qed
 
 lemma (in group_hom) one_closed [simp]:
   "h \<one> \<in> carrier H"

--- a/src/HOL/Algebra/Ideal.thy	Thu Dec 18 11:16:48 2008 +0100
+++ b/src/HOL/Algebra/Ideal.thy	Fri Dec 19 15:05:37 2008 +0100
@@ -13,7 +13,7 @@
 
 subsubsection {* General definition *}
 
-locale ideal = additive_subgroup I R + ring R +
+locale ideal = additive_subgroup I R + ring R for I and R (structure) +
   assumes I_l_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
       and I_r_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
 
@@ -127,7 +127,7 @@
       and I_prime: "\<And>a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I"
   shows "primeideal I R"
 proof -
-  interpret additive_subgroup [I R] by fact
+  interpret additive_subgroup I R by fact
   interpret cring R by fact
   show ?thesis apply (intro_locales)
     apply (intro ideal_axioms.intro)
@@ -207,7 +207,7 @@
   shows "ideal (I \<inter> J) R"
 proof -
   interpret ideal I R by fact
-  interpret ideal [J R] by fact
+  interpret ideal J R by fact
   show ?thesis
 apply (intro idealI subgroup.intro)
       apply (rule is_ring)
@@ -532,7 +532,7 @@
   assumes aJ: "a \<in> J"
   shows "PIdl a \<subseteq> J"
 proof -
-  interpret ideal [J R] by fact
+  interpret ideal J R by fact
   show ?thesis unfolding cgenideal_def
     apply rule
     apply clarify
@@ -579,7 +579,7 @@
   shows "Idl (I \<union> J) = I <+> J"
 apply rule
  apply (rule ring.genideal_minimal)
-   apply (rule R.is_ring)
+   apply (rule is_ring)
   apply (rule add_ideals[OF idealI idealJ])
  apply (rule)
  apply (simp add: set_add_defs) apply (elim disjE) defer 1 defer 1
@@ -829,7 +829,7 @@
       by fast
     def J \<equiv> "{x\<in>carrier R. a \<otimes> x \<in> I}"
     
-    from R.is_cring and acarr
+    from is_cring and acarr
     have idealJ: "ideal J R" unfolding J_def by (rule helper_max_prime)
     
     have IsubJ: "I \<subseteq> J"

--- a/src/HOL/Algebra/IntRing.thy	Thu Dec 18 11:16:48 2008 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Fri Dec 19 15:05:37 2008 +0100
@@ -328,7 +328,7 @@
 next
   assume "UNIV = {uu. EX x. uu = x * p}"
   from this obtain x 
-      where "1 = x * p" by fast
+      where "1 = x * p" by best
   from this [symmetric]
       have "p * x = 1" by (subst zmult_commute)
   hence "\<bar>p * x\<bar> = 1" by simp

--- a/src/HOL/Algebra/Lattice.thy	Thu Dec 18 11:16:48 2008 +0100
+++ b/src/HOL/Algebra/Lattice.thy	Fri Dec 19 15:05:37 2008 +0100
@@ -919,7 +919,7 @@
 
 text {* Total orders are lattices. *}
 
-sublocale weak_total_order < weak_lattice
+sublocale weak_total_order < weak: weak_lattice
 proof
   fix x y
   assume L: "x \<in> carrier L"  "y \<in> carrier L"
@@ -1125,14 +1125,14 @@
   assumes sup_of_two_exists:
     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
 
-sublocale upper_semilattice < weak_upper_semilattice
+sublocale upper_semilattice < weak: weak_upper_semilattice
   proof qed (rule sup_of_two_exists)
 
 locale lower_semilattice = partial_order +
   assumes inf_of_two_exists:
     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
 
-sublocale lower_semilattice < weak_lower_semilattice
+sublocale lower_semilattice < weak: weak_lower_semilattice
   proof qed (rule inf_of_two_exists)
 
 locale lattice = upper_semilattice + lower_semilattice
@@ -1183,7 +1183,7 @@
 locale total_order = partial_order +
   assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
 
-sublocale total_order < weak_total_order
+sublocale total_order < weak: weak_total_order
   proof qed (rule total_order_total)
 
 text {* Introduction rule: the usual definition of total order *}
@@ -1195,7 +1195,7 @@
 
 text {* Total orders are lattices. *}
 
-sublocale total_order < lattice
+sublocale total_order < weak: lattice
   proof qed (auto intro: sup_of_two_exists inf_of_two_exists)
 
 
@@ -1207,7 +1207,7 @@
     and inf_exists:
     "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
 
-sublocale complete_lattice < weak_complete_lattice
+sublocale complete_lattice < weak: weak_complete_lattice
   proof qed (auto intro: sup_exists inf_exists)
 
 text {* Introduction rule: the usual definition of complete lattice *}

--- a/src/HOL/Algebra/QuotRing.thy	Thu Dec 18 11:16:48 2008 +0100
+++ b/src/HOL/Algebra/QuotRing.thy	Fri Dec 19 15:05:37 2008 +0100
@@ -175,9 +175,9 @@
   interpret cring R by fact
   show ?thesis apply (rule ring_hom_cringI)
   apply (rule rcos_ring_hom_ring)
- apply (rule R.is_cring)
+ apply (rule is_cring)
 apply (rule quotient_is_cring)
-apply (rule R.is_cring)
+apply (rule is_cring)
 done
 qed
 

--- a/src/HOL/Algebra/RingHom.thy	Thu Dec 18 11:16:48 2008 +0100
+++ b/src/HOL/Algebra/RingHom.thy	Fri Dec 19 15:05:37 2008 +0100
@@ -10,16 +10,17 @@
 section {* Homomorphisms of Non-Commutative Rings *}
 
 text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
-locale ring_hom_ring = R: ring R + S: ring S +
+locale ring_hom_ring = R: ring R + S: ring S
+    for R (structure) and S (structure) +
   fixes h
   assumes homh: "h \<in> ring_hom R S"
   notes hom_mult [simp] = ring_hom_mult [OF homh]
     and hom_one [simp] = ring_hom_one [OF homh]
 
-sublocale ring_hom_cring \<subseteq> ring_hom_ring
+sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring
   proof qed (rule homh)
 
-sublocale ring_hom_ring \<subseteq> abelian_group_hom R S
+sublocale ring_hom_ring \<subseteq> abelian_group: abelian_group_hom R S
 apply (rule abelian_group_homI)
   apply (rule R.is_abelian_group)
  apply (rule S.is_abelian_group)

--- a/src/HOL/Algebra/UnivPoly.thy	Thu Dec 18 11:16:48 2008 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Fri Dec 19 15:05:37 2008 +0100
@@ -175,17 +175,17 @@
   fixes R (structure) and P (structure)
   defines P_def: "P == UP R"
 
-locale UP_ring = UP + ring R
+locale UP_ring = UP + R: ring R
 
-locale UP_cring = UP + cring R
+locale UP_cring = UP + R: cring R
 
 sublocale UP_cring < UP_ring
-  by (rule P_def) intro_locales
+  by intro_locales [1] (rule P_def)
 
-locale UP_domain = UP + "domain" R
+locale UP_domain = UP + R: "domain" R
 
 sublocale UP_domain < UP_cring
-  by (rule P_def) intro_locales
+  by intro_locales [1] (rule P_def)
 
 context UP
 begin
@@ -457,8 +457,8 @@
 
 end
 
-sublocale UP_ring < ring P using UP_ring .
-sublocale UP_cring < cring P using UP_cring .
+sublocale UP_ring < P: ring P using UP_ring .
+sublocale UP_cring < P: cring P using UP_cring .
 
 
 subsection {* Polynomials Form an Algebra *}
@@ -1203,7 +1203,9 @@
 
 text {* The universal property of the polynomial ring *}
 
-locale UP_pre_univ_prop = ring_hom_cring R S h + UP_cring R P
+locale UP_pre_univ_prop = ring_hom_cring + UP_cring
+
+(* FIXME print_locale ring_hom_cring fails *)
 
 locale UP_univ_prop = UP_pre_univ_prop +
   fixes s and Eval
@@ -1771,7 +1773,7 @@
   shows "eval R R id a (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = \<zero>"
   (is "eval R R id a ?g = _")
 proof -
-  interpret UP_pre_univ_prop R R id P proof qed simp
+  interpret UP_pre_univ_prop R R id proof qed simp
   have eval_ring_hom: "eval R R id a \<in> ring_hom P R" using eval_ring_hom [OF a] by simp
   interpret ring_hom_cring P R "eval R R id a" proof qed (simp add: eval_ring_hom)
   have mon1_closed: "monom P \<one>\<^bsub>R\<^esub> 1 \<in> carrier P" 
@@ -1780,8 +1782,8 @@
     using a R.a_inv_closed by auto
   have "eval R R id a ?g = eval R R id a (monom P \<one> 1) \<ominus> eval R R id a (monom P a 0)"
     unfolding P.minus_eq [OF mon1_closed mon0_closed]
-    unfolding R_S_h.hom_add [OF mon1_closed min_mon0_closed]
-    unfolding R_S_h.hom_a_inv [OF mon0_closed] 
+    unfolding hom_add [OF mon1_closed min_mon0_closed]
+    unfolding hom_a_inv [OF mon0_closed] 
     using R.minus_eq [symmetric] mon1_closed mon0_closed by auto
   also have "\<dots> = a \<ominus> a"
     using eval_monom [OF R.one_closed a, of 1] using eval_monom [OF a a, of 0] using a by simp
@@ -1884,7 +1886,7 @@
   "UP INTEG"} globally.
 *}
 
-interpretation INTEG!: UP_pre_univ_prop INTEG INTEG id
+interpretation INTEG!: UP_pre_univ_prop INTEG INTEG id "UP INTEG"
   using INTEG_id_eval by simp_all
 
 lemma INTEG_closed [intro, simp]:

--- a/src/HOL/Statespace/StateSpaceEx.thy	Thu Dec 18 11:16:48 2008 +0100
+++ b/src/HOL/Statespace/StateSpaceEx.thy	Fri Dec 19 15:05:37 2008 +0100
@@ -202,8 +202,10 @@
 
 text {* Hmm, I hoped this would work now...*}
 
+(*
 locale fooX = foo +
  assumes "s<a:=i>\<cdot>b = k"
+*)
 
 (* ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ *)
 text {* There are known problems with syntax-declarations. They currently

--- a/src/HOLCF/CompactBasis.thy	Thu Dec 18 11:16:48 2008 +0100
+++ b/src/HOLCF/CompactBasis.thy	Fri Dec 19 15:05:37 2008 +0100
@@ -244,7 +244,7 @@
   assumes "ab_semigroup_idem_mult f"
   shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
 proof -
-  interpret ab_semigroup_idem_mult f by fact
+  class_interpret ab_semigroup_idem_mult [f] by fact
   show ?thesis unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
 qed
 

--- a/src/HOLCF/ConvexPD.thy	Thu Dec 18 11:16:48 2008 +0100
+++ b/src/HOLCF/ConvexPD.thy	Fri Dec 19 15:05:37 2008 +0100
@@ -296,7 +296,7 @@
 apply (simp add: PDPlus_absorb)
 done
 
-interpretation aci_convex_plus!: ab_semigroup_idem_mult "op +\<natural>"
+class_interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\<natural>"]
   by unfold_locales
     (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+
 

--- a/src/HOLCF/LowerPD.thy	Thu Dec 18 11:16:48 2008 +0100
+++ b/src/HOLCF/LowerPD.thy	Fri Dec 19 15:05:37 2008 +0100
@@ -250,7 +250,7 @@
 apply (simp add: PDPlus_absorb)
 done
 
-interpretation aci_lower_plus!: ab_semigroup_idem_mult "op +\<flat>"
+class_interpretation aci_lower_plus: ab_semigroup_idem_mult ["op +\<flat>"]
   by unfold_locales
     (rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+
 

--- a/src/HOLCF/UpperPD.thy	Thu Dec 18 11:16:48 2008 +0100
+++ b/src/HOLCF/UpperPD.thy	Fri Dec 19 15:05:37 2008 +0100
@@ -248,7 +248,7 @@
 apply (simp add: PDPlus_absorb)
 done
 
-interpretation aci_upper_plus!: ab_semigroup_idem_mult "op +\<sharp>"
+class_interpretation aci_upper_plus: ab_semigroup_idem_mult ["op +\<sharp>"]
   by unfold_locales
     (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+
 

--- a/src/Pure/Isar/expression.ML	Thu Dec 18 11:16:48 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Fri Dec 19 15:05:37 2008 +0100
@@ -271,38 +271,7 @@
   | declare_elem _ (Defines _) ctxt = ctxt
   | declare_elem _ (Notes _) ctxt = ctxt;
 
-(** Finish locale elements, extract specification text **)
-
-val norm_term = Envir.beta_norm oo Term.subst_atomic;
-
-fun bind_def ctxt eq (xs, env, eqs) =
-  let
-    val _ = LocalDefs.cert_def ctxt eq;
-    val ((y, T), b) = LocalDefs.abs_def eq;
-    val b' = norm_term env b;
-    fun err msg = error (msg ^ ": " ^ quote y);
-  in
-    exists (fn (x, _) => x = y) xs andalso
-      err "Attempt to define previously specified variable";
-    exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
-      err "Attempt to redefine variable";
-    (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs)
-  end;
-
-fun eval_text _ _ (Fixes _) text = text
-  | eval_text _ _ (Constrains _) text = text
-  | eval_text _ is_ext (Assumes asms)
-        (((exts, exts'), (ints, ints')), (xs, env, defs)) =
-      let
-        val ts = maps (map #1 o #2) asms;
-        val ts' = map (norm_term env) ts;
-        val spec' =
-          if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
-          else ((exts, exts'), (ints @ ts, ints' @ ts'));
-      in (spec', (fold Term.add_frees ts' xs, env, defs)) end
-  | eval_text ctxt _ (Defines defs) (spec, binds) =
-      (spec, fold (bind_def ctxt o #1 o #2) defs binds)
-  | eval_text _ _ (Notes _) text = text;
+(** Finish locale elements **)
 
 fun closeup _ _ false elem = elem
   | closeup ctxt parms true elem =
@@ -337,36 +306,24 @@
   | finish_primitive _ close (Defines defs) = close (Defines defs)
   | finish_primitive _ _ (Notes facts) = Notes facts;
 
-fun finish_inst ctxt parms do_close (loc, (prfx, inst)) text =
+fun finish_inst ctxt parms do_close (loc, (prfx, inst)) =
   let
     val thy = ProofContext.theory_of ctxt;
     val (parm_names, parm_types) = NewLocale.params_of thy loc |>
       map (fn (b, SOME T, _) => (Binding.base_name b, T)) |> split_list;
-    val (asm, defs) = NewLocale.specification_of thy loc;
     val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
-    val asm' = Option.map (Morphism.term morph) asm;
-    val defs' = map (Morphism.term morph) defs;
-    val text' = text |>
-      (if is_some asm
-        then eval_text ctxt false (Assumes [(Attrib.empty_binding, [(the asm', [])])])
-        else I) |>
-      (if not (null defs)
-        then eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs'))
-        else I)
-(* FIXME clone from new_locale.ML *)
-  in ((loc, morph), text') end;
+  in (loc, morph) end;
 
-fun finish_elem ctxt parms do_close elem text =
+fun finish_elem ctxt parms do_close elem =
   let
     val elem' = finish_primitive parms (closeup ctxt parms do_close) elem;
-    val text' = eval_text ctxt true elem' text;
-  in (elem', text') end
+  in elem' end
   
-fun finish ctxt parms do_close insts elems text =
+fun finish ctxt parms do_close insts elems =
   let
-    val (deps, text') = fold_map (finish_inst ctxt parms do_close) insts text;
-    val (elems', text'') = fold_map (finish_elem ctxt parms do_close) elems text';
-  in (deps, elems', text'') end;
+    val deps = map (finish_inst ctxt parms do_close) insts;
+    val elems' = map (finish_elem ctxt parms do_close) elems;
+  in (deps, elems') end;
 
 
 (** Process full context statement: instantiations + elements + conclusion **)
@@ -422,28 +379,9 @@
     val parms = xs ~~ Ts;  (* params from expression and elements *)
 
     val Fixes fors' = finish_primitive parms I (Fixes fors);
-    val (deps, elems', text) = finish ctxt' parms do_close insts elems ((([], []), ([], [])), ([], [], []));
-    (* text has the following structure:
-           (((exts, exts'), (ints, ints')), (xs, env, defs))
-       where
-         exts: external assumptions (terms in assumes elements)
-         exts': dito, normalised wrt. env
-         ints: internal assumptions (terms in assumptions from insts)
-         ints': dito, normalised wrt. env
-         xs: the free variables in exts' and ints' and rhss of definitions,
-           this includes parameters except defined parameters
-         env: list of term pairs encoding substitutions, where the first term
-           is a free variable; substitutions represent defines elements and
-           the rhs is normalised wrt. the previous env
-         defs: the equations from the defines elements
-       elems is an updated version of raw_elems:
-         - type info added to Fixes and modified in Constrains
-         - axiom and definition statement replaced by corresponding one
-           from proppss in Assumes and Defines
-         - Facts unchanged
-       *)
+    val (deps, elems') = finish ctxt' parms do_close insts elems;
 
-  in ((fors', deps, elems', concl), (parms, text)) end
+  in ((fors', deps, elems', concl), (parms, ctxt')) end
 
 in
 
@@ -480,14 +418,13 @@
 
 fun prep_declaration prep activate raw_import raw_elems context =
   let
-    val ((fixed, deps, elems, _), (parms, (spec, (_, _, defs)))) =
-      prep false true context raw_import raw_elems [];
+    val ((fixed, deps, elems, _), (parms, ctxt')) = prep false true context raw_import raw_elems [];
     (* Declare parameters and imported facts *)
     val context' = context |>
       ProofContext.add_fixes_i fixed |> snd |>
       fold NewLocale.activate_local_facts deps;
     val (elems', _) = activate elems (ProofContext.set_stmt true context');
-  in ((fixed, deps, elems'), (parms, spec, defs)) end;
+  in ((fixed, deps, elems'), (parms, ctxt')) end;
 
 in
 
@@ -522,8 +459,7 @@
 
     val export = Variable.export_morphism goal_ctxt context;
     val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
-    val thy_ref = Theory.check_thy thy; (* FIXME!!*)
-    val exp_term = (fn t => Drule.term_rule (Theory.deref thy_ref) (singleton exp_fact) t);
+    val exp_term = TermSubst.zero_var_indexes o Morphism.term export;
     val exp_typ = Logic.type_map exp_term;
     val export' =
       Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
@@ -539,6 +475,81 @@
 
 (*** Locale declarations ***)
 
+(* extract specification text *)
+
+val norm_term = Envir.beta_norm oo Term.subst_atomic;
+
+fun bind_def ctxt eq (xs, env, eqs) =
+  let
+    val _ = LocalDefs.cert_def ctxt eq;
+    val ((y, T), b) = LocalDefs.abs_def eq;
+    val b' = norm_term env b;
+    fun err msg = error (msg ^ ": " ^ quote y);
+  in
+    exists (fn (x, _) => x = y) xs andalso
+      err "Attempt to define previously specified variable";
+    exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
+      err "Attempt to redefine variable";
+    (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs)
+  end;
+
+(* text has the following structure:
+       (((exts, exts'), (ints, ints')), (xs, env, defs))
+   where
+     exts: external assumptions (terms in assumes elements)
+     exts': dito, normalised wrt. env
+     ints: internal assumptions (terms in assumptions from insts)
+     ints': dito, normalised wrt. env
+     xs: the free variables in exts' and ints' and rhss of definitions,
+       this includes parameters except defined parameters
+     env: list of term pairs encoding substitutions, where the first term
+       is a free variable; substitutions represent defines elements and
+       the rhs is normalised wrt. the previous env
+     defs: the equations from the defines elements
+   *)
+
+fun eval_text _ _ (Fixes _) text = text
+  | eval_text _ _ (Constrains _) text = text
+  | eval_text _ is_ext (Assumes asms)
+        (((exts, exts'), (ints, ints')), (xs, env, defs)) =
+      let
+        val ts = maps (map #1 o #2) asms;
+        val ts' = map (norm_term env) ts;
+        val spec' =
+          if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
+          else ((exts, exts'), (ints @ ts, ints' @ ts'));
+      in (spec', (fold Term.add_frees ts' xs, env, defs)) end
+  | eval_text ctxt _ (Defines defs) (spec, binds) =
+      (spec, fold (bind_def ctxt o #1 o #2) defs binds)
+  | eval_text _ _ (Notes _) text = text;
+
+fun eval_inst ctxt (loc, morph) text =
+  let
+    val thy = ProofContext.theory_of ctxt;
+    val (asm, defs) = NewLocale.specification_of thy loc;
+    val asm' = Option.map (Morphism.term morph) asm;
+    val defs' = map (Morphism.term morph) defs;
+    val text' = text |>
+      (if is_some asm
+        then eval_text ctxt false (Assumes [(Attrib.empty_binding, [(the asm', [])])])
+        else I) |>
+      (if not (null defs)
+        then eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs'))
+        else I)
+(* FIXME clone from new_locale.ML *)
+  in text' end;
+
+fun eval_elem ctxt elem text =
+  let
+    val text' = eval_text ctxt true elem text;
+  in text' end;
+
+fun eval ctxt deps elems =
+  let
+    val text' = fold (eval_inst ctxt) deps ((([], []), ([], [])), ([], [], []));
+    val ((spec, (_, _, defs))) = fold (eval_elem ctxt) elems text';
+  in (spec, defs) end;
+
 (* axiomsN: name of theorem set with destruct rules for locale predicates,
      also name suffix of delta predicates and assumptions. *)
 
@@ -624,7 +635,7 @@
 
 (* CB: main predicate definition function *)
 
-fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) thy =
+fun define_preds pname parms (((exts, exts'), (ints, ints')), defs) thy =
   let
     val defs' = map (cterm_of thy #> Assumption.assume #> Drule.gen_all #> Drule.abs_def) defs;
 
@@ -677,7 +688,8 @@
 
 fun defines_to_notes thy (Defines defs) =
       Notes (Thm.definitionK, map (fn (a, (def, _)) =>
-        (a, [([Assumption.assume (cterm_of thy def)], [])])) defs)
+        (a, [([Assumption.assume (cterm_of thy def)],
+          [(Attrib.internal o K) NewLocale.witness_attrib])])) defs)
   | defines_to_notes _ e = e;
 
 fun gen_add_locale prep_decl
@@ -687,10 +699,12 @@
     val _ = NewLocale.test_locale thy name andalso
       error ("Duplicate definition of locale " ^ quote name);
 
-    val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), defs)) =
+    val ((fixed, deps, body_elems), (parms, ctxt')) =
       prep_decl raw_imprt raw_body (ProofContext.init thy);
+    val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
+
     val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
-      define_preds predicate_name text thy;
+      define_preds predicate_name parms text thy;
 
     val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
     val _ = if null extraTs then ()

--- a/src/Pure/Isar/new_locale.ML	Thu Dec 18 11:16:48 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Fri Dec 19 15:05:37 2008 +0100
@@ -375,8 +375,8 @@
     val ctxt = init name' thy
   in
     Pretty.big_list "locale elements:"
-      (activate_all name' thy (cons_elem show_facts) (K Morphism.identity) (empty, []) |>
-        snd |> rev |> 
+      (activate_all name' thy (cons_elem show_facts) (K (Element.transfer_morphism thy))
+        (empty, []) |> snd |> rev |> 
         map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
   end
 
@@ -399,9 +399,15 @@
 
 val get_global_registrations =
   Context.Theory #> RegistrationsData.get #> map fst #> map (apsnd op $>);
-fun add_global_registration reg =
+
+fun add_global reg =
   (Context.theory_map o RegistrationsData.map) (cons (reg, stamp ()));
 
+fun add_global_registration (name, (base_morph, export)) thy =
+  roundup thy (fn _ => fn (name', morph') => fn thy => add_global (name', (morph', export)) thy)
+    (name, base_morph) (get_global_idents thy, thy) |>
+    snd (* FIXME ?? uncurry put_global_idents *);
+
 fun amend_global_registration morph (name, base_morph) thy =
   let
     val regs = (Context.Theory #> RegistrationsData.get #> map fst) thy;