# HG changeset patch
# User ballarin
# Date 1229627989 -3600
# Node ID 3adc06d6504f2ef6fba41e309d06293cef2757aa
# Parent  918687637307cdedf9b9c5ae9fc4f416b2c95cc6# Parent  bb81c3709fb689dbb2a37678bbc33d87b53542aa
Merged.

diff -r 918687637307 -r 3adc06d6504f etc/isar-keywords-ZF.el
diff -r 918687637307 -r 3adc06d6504f etc/isar-keywords.el
--- a/etc/isar-keywords.el	Thu Dec 18 19:52:11 2008 +0100
+++ b/etc/isar-keywords.el	Thu Dec 18 20:19:49 2008 +0100
@@ -45,6 +45,9 @@
     "chapter"
     "class"
     "class_deps"
+    "class_interpret"
+    "class_interpretation"
+    "class_locale"
     "classes"
     "classrel"
     "code_abort"
@@ -418,6 +421,7 @@
     "axiomatization"
     "axioms"
     "class"
+    "class_locale"
     "classes"
     "classrel"
     "code_abort"
@@ -501,6 +505,7 @@
 
 (defconst isar-keywords-theory-goal
   '("ax_specification"
+    "class_interpretation"
     "corollary"
     "cpodef"
     "function"
@@ -539,7 +544,8 @@
     "subsubsect"))
 
 (defconst isar-keywords-proof-goal
-  '("have"
+  '("class_interpret"
+    "have"
     "hence"
     "interpret"
     "invoke"))
diff -r 918687637307 -r 3adc06d6504f src/HOL/Algebra/AbelCoset.thy
--- a/src/HOL/Algebra/AbelCoset.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,6 +1,5 @@
 (*
   Title:     HOL/Algebra/AbelCoset.thy
-  Id:        $Id$
   Author:    Stephan Hohe, TU Muenchen
 *)
 
@@ -52,7 +51,9 @@
   "a_kernel G H h \<equiv> kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
                               \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
 
-locale abelian_group_hom = abelian_group G + abelian_group H + var h +
+locale abelian_group_hom = G: abelian_group G + H: abelian_group H
+    for G (structure) and H (structure) +
+  fixes h
   assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
                                   (| carrier = carrier H, mult = add H, one = zero H |) h"
 
@@ -180,7 +181,8 @@
 
 subsubsection {* Subgroups *}
 
-locale additive_subgroup = var H + struct G +
+locale additive_subgroup =
+  fixes H and G (structure)
   assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
 
 lemma (in additive_subgroup) is_additive_subgroup:
@@ -218,7 +220,7 @@
 
 text {* Every subgroup of an @{text "abelian_group"} is normal *}
 
-locale abelian_subgroup = additive_subgroup H G + abelian_group G +
+locale abelian_subgroup = additive_subgroup + abelian_group G +
   assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
 
 lemma (in abelian_subgroup) is_abelian_subgroup:
@@ -230,7 +232,7 @@
       and a_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus>\<^bsub>G\<^esub> y = y \<oplus>\<^bsub>G\<^esub> x"
   shows "abelian_subgroup H G"
 proof -
-  interpret normal ["H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
+  interpret normal "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   by (rule a_normal)
 
   show "abelian_subgroup H G"
@@ -243,9 +245,9 @@
       and a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   shows "abelian_subgroup H G"
 proof -
-  interpret comm_group ["\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
+  interpret comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   by (rule a_comm_group)
-  interpret subgroup ["H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
+  interpret subgroup "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   by (rule a_subgroup)
 
   show "abelian_subgroup H G"
@@ -538,8 +540,8 @@
                                   (| carrier = carrier H, mult = add H, one = zero H |) h"
   shows "abelian_group_hom G H h"
 proof -
-  interpret G: abelian_group [G] by fact
-  interpret H: abelian_group [H] by fact
+  interpret G!: abelian_group G by fact
+  interpret H!: abelian_group H by fact
   show ?thesis apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
     apply fact
     apply fact
@@ -690,7 +692,7 @@
   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
   shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
 proof -
-  interpret G: ring [G] by fact
+  interpret G!: ring G by fact
   from carr
   have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
   with carr
diff -r 918687637307 -r 3adc06d6504f src/HOL/Algebra/Congruence.thy
--- a/src/HOL/Algebra/Congruence.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Algebra/Congruence.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,6 +1,5 @@
 (*
   Title:  Algebra/Congruence.thy
-  Id:     $Id$
   Author: Clemens Ballarin, started 3 January 2008
   Copyright: Clemens Ballarin
 *)
diff -r 918687637307 -r 3adc06d6504f src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Algebra/Coset.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Algebra/Coset.thy
-    ID:         $Id$
     Author:     Florian Kammueller, with new proofs by L C Paulson, and
                 Stephan Hohe
 *)
@@ -114,7 +113,7 @@
       and repr:  "H #> x = H #> y"
   shows "y \<in> H #> x"
 proof -
-  interpret subgroup [H G] by fact
+  interpret subgroup H G by fact
   show ?thesis  apply (subst repr)
   apply (intro rcos_self)
    apply (rule ycarr)
@@ -129,7 +128,7 @@
     and a': "a' \<in> H #> a"
   shows "a' \<in> carrier G"
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   from subset and acarr
   have "H #> a \<subseteq> carrier G" by (rule r_coset_subset_G)
   from this and a'
@@ -142,7 +141,7 @@
   assumes hH: "h \<in> H"
   shows "H #> h = H"
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   show ?thesis apply (unfold r_coset_def)
     apply rule
     apply rule
@@ -173,7 +172,7 @@
       and x'cos: "x' \<in> H #> x"
   shows "(x' \<otimes> inv x) \<in> H"
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   from xcarr x'cos
       have x'carr: "x' \<in> carrier G"
       by (rule elemrcos_carrier[OF is_group])
@@ -213,7 +212,7 @@
       and xixH: "(x' \<otimes> inv x) \<in> H"
   shows "x' \<in> H #> x"
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   from xixH
       have "\<exists>h\<in>H. x' \<otimes> (inv x) = h" by fast
   from this
@@ -244,7 +243,7 @@
   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
   shows "(x' \<in> H #> x) = (x' \<otimes> inv x \<in> H)"
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   show ?thesis proof  assume "x' \<in> H #> x"
     from this and carr
     show "x' \<otimes> inv x \<in> H"
@@ -263,7 +262,7 @@
   assumes XH: "X \<in> rcosets H"
   shows "X \<subseteq> carrier G"
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   from XH have "\<exists>x\<in> carrier G. X = H #> x"
       unfolding RCOSETS_def
       by fast
@@ -348,7 +347,7 @@
       and xixH: "(inv x \<otimes> x') \<in> H"
   shows "x' \<in> x <# H"
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   from xixH
       have "\<exists>h\<in>H. (inv x) \<otimes> x' = h" by fast
   from this
@@ -600,7 +599,7 @@
    assumes "group G"
    shows "equiv (carrier G) (rcong H)"
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   show ?thesis
   proof (intro equiv.intro)
     show "refl (carrier G) (rcong H)"
@@ -647,7 +646,7 @@
   assumes a: "a \<in> carrier G"
   shows "a <# H = rcong H `` {a}"
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) 
 qed
 
@@ -658,7 +657,7 @@
   assumes p: "ha \<otimes> a = h \<otimes> b" "a \<in> carrier G" "b \<in> carrier G" "h \<in> H" "ha \<in> H" "hb \<in> H"
   shows "hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
 proof -
-  interpret subgroup [H G] by fact
+  interpret subgroup H G by fact
   from p show ?thesis apply (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
     apply (simp add: )
     apply (simp add: m_assoc transpose_inv)
@@ -670,7 +669,7 @@
   assumes p: "a \<in> rcosets H" "b \<in> rcosets H" "a\<noteq>b"
   shows "a \<inter> b = {}"
 proof -
-  interpret subgroup [H G] by fact
+  interpret subgroup H G by fact
   from p show ?thesis apply (simp add: RCOSETS_def r_coset_def)
     apply (blast intro: rcos_equation prems sym)
     done
@@ -760,7 +759,7 @@
   assumes "subgroup H G"
   shows "\<Union>(rcosets H) = carrier G"
 proof -
-  interpret subgroup [H G] by fact
+  interpret subgroup H G by fact
   show ?thesis
     apply (rule equalityI)
     apply (force simp add: RCOSETS_def r_coset_def)
@@ -847,7 +846,7 @@
   assumes "group G"
   shows "H \<in> rcosets H"
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   from _ subgroup_axioms have "H #> \<one> = H"
     by (rule coset_join2) auto
   then show ?thesis
diff -r 918687637307 -r 3adc06d6504f src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,6 +1,5 @@
 (*
   Title:     Divisibility in monoids and rings
-  Id:        $Id$
   Author:    Clemens Ballarin, started 18 July 2008
 
 Based on work by Stephan Hohe.
@@ -32,7 +31,7 @@
   "monoid_cancel G"
   ..
 
-interpretation group \<subseteq> monoid_cancel
+sublocale group \<subseteq> monoid_cancel
   proof qed simp+
 
 
@@ -45,7 +44,7 @@
           "\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
   shows "comm_monoid_cancel G"
 proof -
-  interpret comm_monoid [G] by fact
+  interpret comm_monoid G by fact
   show "comm_monoid_cancel G"
     apply unfold_locales
     apply (subgoal_tac "a \<otimes> c = b \<otimes> c")
@@ -59,7 +58,7 @@
   "comm_monoid_cancel G"
   by intro_locales
 
-interpretation comm_group \<subseteq> comm_monoid_cancel
+sublocale comm_group \<subseteq> comm_monoid_cancel
   ..
 
 
@@ -755,7 +754,7 @@
 using pf
 unfolding properfactor_lless
 proof -
-  interpret weak_partial_order ["division_rel G"] ..
+  interpret weak_partial_order "division_rel G" ..
   from x'x
        have "x' .=\<^bsub>division_rel G\<^esub> x" by simp
   also assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
@@ -771,7 +770,7 @@
 using pf
 unfolding properfactor_lless
 proof -
-  interpret weak_partial_order ["division_rel G"] ..
+  interpret weak_partial_order "division_rel G" ..
   assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
   also from yy'
        have "y .=\<^bsub>division_rel G\<^esub> y'" by simp
@@ -2916,7 +2915,7 @@
 lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]:
   shows "weak_lower_semilattice (division_rel G)"
 proof -
-  interpret weak_partial_order ["division_rel G"] ..
+  interpret weak_partial_order "division_rel G" ..
   show ?thesis
   apply (unfold_locales, simp_all)
   proof -
@@ -2941,7 +2940,7 @@
   shows "a' gcdof b c"
 proof -
   note carr = a'carr carr'
-  interpret weak_lower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice "division_rel G" by simp
   have "a' \<in> carrier G \<and> a' gcdof b c"
     apply (simp add: gcdof_greatestLower carr')
     apply (subst greatest_Lower_cong_l[of _ a])
@@ -2958,7 +2957,7 @@
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "somegcd G a b \<in> carrier G"
 proof -
-  interpret weak_lower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
     apply (simp add: somegcd_meet[OF carr])
     apply (rule meet_closed[simplified], fact+)
@@ -2969,7 +2968,7 @@
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "(somegcd G a b) gcdof a b"
 proof -
-  interpret weak_lower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice "division_rel G" by simp
   from carr
   have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"
     apply (subst gcdof_greatestLower, simp, simp)
@@ -2983,7 +2982,7 @@
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "\<exists>x\<in>carrier G. x = somegcd G a b"
 proof -
-  interpret weak_lower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
     apply (simp add: somegcd_meet[OF carr])
     apply (rule meet_closed[simplified], fact+)
@@ -2994,7 +2993,7 @@
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "(somegcd G a b) divides a"
 proof -
-  interpret weak_lower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
     apply (simp add: somegcd_meet[OF carr])
     apply (rule meet_left[simplified], fact+)
@@ -3005,7 +3004,7 @@
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "(somegcd G a b) divides b"
 proof -
-  interpret weak_lower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
     apply (simp add: somegcd_meet[OF carr])
     apply (rule meet_right[simplified], fact+)
@@ -3017,7 +3016,7 @@
     and L: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   shows "z divides (somegcd G x y)"
 proof -
-  interpret weak_lower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
     apply (simp add: somegcd_meet L)
     apply (rule meet_le[simplified], fact+)
@@ -3029,7 +3028,7 @@
     and carr: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
   shows "somegcd G x y \<sim> somegcd G x' y"
 proof -
-  interpret weak_lower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
     apply (simp add: somegcd_meet carr)
     apply (rule meet_cong_l[simplified], fact+)
@@ -3041,7 +3040,7 @@
     and yy': "y \<sim> y'"
   shows "somegcd G x y \<sim> somegcd G x y'"
 proof -
-  interpret weak_lower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
     apply (simp add: somegcd_meet carr)
     apply (rule meet_cong_r[simplified], fact+)
@@ -3092,7 +3091,7 @@
   assumes "finite A"  "A \<subseteq> carrier G"  "A \<noteq> {}"
   shows "\<exists>x\<in> carrier G. x = SomeGcd G A"
 proof -
-  interpret weak_lower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
     apply (simp add: SomeGcd_def)
     apply (rule finite_inf_closed[simplified], fact+)
@@ -3103,7 +3102,7 @@
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   shows "somegcd G (somegcd G a b) c \<sim> somegcd G a (somegcd G b c)"
 proof -
-  interpret weak_lower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
     apply (subst (2 3) somegcd_meet, (simp add: carr)+)
     apply (simp add: somegcd_meet carr)
@@ -3313,7 +3312,7 @@
   qed
 qed
 
-interpretation gcd_condition_monoid \<subseteq> primeness_condition_monoid
+sublocale gcd_condition_monoid \<subseteq> primeness_condition_monoid
   by (rule primeness_condition)
 
 
@@ -3832,7 +3831,7 @@
   with fca fcb show ?thesis by simp
 qed
 
-interpretation factorial_monoid \<subseteq> divisor_chain_condition_monoid
+sublocale factorial_monoid \<subseteq> divisor_chain_condition_monoid
 apply unfold_locales
 apply (rule wfUNIVI)
 apply (rule measure_induct[of "factorcount G"])
@@ -3854,7 +3853,7 @@
   done
 qed
 
-interpretation factorial_monoid \<subseteq> primeness_condition_monoid
+sublocale factorial_monoid \<subseteq> primeness_condition_monoid
   proof qed (rule irreducible_is_prime)
 
 
@@ -3866,13 +3865,13 @@
   shows "gcd_condition_monoid G"
   proof qed (rule gcdof_exists)
 
-interpretation factorial_monoid \<subseteq> gcd_condition_monoid
+sublocale factorial_monoid \<subseteq> gcd_condition_monoid
   proof qed (rule gcdof_exists)
 
 lemma (in factorial_monoid) division_weak_lattice [simp]:
   shows "weak_lattice (division_rel G)"
 proof -
-  interpret weak_lower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice "division_rel G" by simp
 
   show "weak_lattice (division_rel G)"
   apply (unfold_locales, simp_all)
@@ -3902,14 +3901,14 @@
 proof clarify
   assume dcc: "divisor_chain_condition_monoid G"
      and pc: "primeness_condition_monoid G"
-  interpret divisor_chain_condition_monoid ["G"] by (rule dcc)
-  interpret primeness_condition_monoid ["G"] by (rule pc)
+  interpret divisor_chain_condition_monoid "G" by (rule dcc)
+  interpret primeness_condition_monoid "G" by (rule pc)
 
   show "factorial_monoid G"
       by (fast intro: factorial_monoidI wfactors_exist wfactors_unique)
 next
   assume fm: "factorial_monoid G"
-  interpret factorial_monoid ["G"] by (rule fm)
+  interpret factorial_monoid "G" by (rule fm)
   show "divisor_chain_condition_monoid G \<and> primeness_condition_monoid G"
       by rule unfold_locales
 qed
@@ -3920,13 +3919,13 @@
 proof clarify
     assume dcc: "divisor_chain_condition_monoid G"
      and gc: "gcd_condition_monoid G"
-  interpret divisor_chain_condition_monoid ["G"] by (rule dcc)
-  interpret gcd_condition_monoid ["G"] by (rule gc)
+  interpret divisor_chain_condition_monoid "G" by (rule dcc)
+  interpret gcd_condition_monoid "G" by (rule gc)
   show "factorial_monoid G"
       by (simp add: factorial_condition_one[symmetric], rule, unfold_locales)
 next
   assume fm: "factorial_monoid G"
-  interpret factorial_monoid ["G"] by (rule fm)
+  interpret factorial_monoid "G" by (rule fm)
   show "divisor_chain_condition_monoid G \<and> gcd_condition_monoid G"
       by rule unfold_locales
 qed
diff -r 918687637307 -r 3adc06d6504f src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Algebra/FiniteProduct.thy
-    ID:         $Id$
     Author:     Clemens Ballarin, started 19 November 2002
 
 This file is largely based on HOL/Finite_Set.thy.
@@ -519,9 +518,9 @@
 lemma finprod_singleton:
   assumes i_in_A: "i \<in> A" and fin_A: "finite A" and f_Pi: "f \<in> A \<rightarrow> carrier G"
   shows "(\<Otimes>j\<in>A. if i = j then f j else \<one>) = f i"
-  using i_in_A G.finprod_insert [of "A - {i}" i "(\<lambda>j. if i = j then f j else \<one>)"]
-    fin_A f_Pi G.finprod_one [of "A - {i}"]
-    G.finprod_cong [of "A - {i}" "A - {i}" "(\<lambda>j. if i = j then f j else \<one>)" "(\<lambda>i. \<one>)"] 
+  using i_in_A finprod_insert [of "A - {i}" i "(\<lambda>j. if i = j then f j else \<one>)"]
+    fin_A f_Pi finprod_one [of "A - {i}"]
+    finprod_cong [of "A - {i}" "A - {i}" "(\<lambda>j. if i = j then f j else \<one>)" "(\<lambda>i. \<one>)"] 
   unfolding Pi_def simp_implies_def by (force simp add: insert_absorb)
 
 end
diff -r 918687637307 -r 3adc06d6504f src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Algebra/Group.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,6 +1,5 @@
 (*
   Title:  HOL/Algebra/Group.thy
-  Id:     $Id$
   Author: Clemens Ballarin, started 4 February 2003
 
 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
@@ -425,7 +424,7 @@
   assumes "group G"
   shows "group (G\<lparr>carrier := H\<rparr>)"
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   show ?thesis
     apply (rule monoid.group_l_invI)
     apply (unfold_locales) [1]
@@ -489,8 +488,8 @@
   assumes "monoid G" and "monoid H"
   shows "monoid (G \<times>\<times> H)"
 proof -
-  interpret G: monoid [G] by fact
-  interpret H: monoid [H] by fact
+  interpret G!: monoid G by fact
+  interpret H!: monoid H by fact
   from assms
   show ?thesis by (unfold monoid_def DirProd_def, auto) 
 qed
@@ -501,8 +500,8 @@
   assumes "group G" and "group H"
   shows "group (G \<times>\<times> H)"
 proof -
-  interpret G: group [G] by fact
-  interpret H: group [H] by fact
+  interpret G!: group G by fact
+  interpret H!: group H by fact
   show ?thesis by (rule groupI)
      (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
            simp add: DirProd_def)
@@ -526,9 +525,9 @@
       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 -
-  interpret G: group [G] by fact
-  interpret H: group [H] by fact
-  interpret Prod: group ["G \<times>\<times> H"]
+  interpret G!: group G by fact
+  interpret H!: group H by fact
+  interpret Prod!: group "G \<times>\<times> H"
     by (auto intro: DirProd_group group.intro group.axioms assms)
   show ?thesis by (simp add: Prod.inv_equality g h)
 qed
@@ -542,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) 
@@ -587,10 +577,23 @@
 
 text{*Basis for homomorphism proofs: we assume two groups @{term G} and
   @{term H}, with a homomorphism @{term h} between them*}
-locale group_hom = group G + group H + var h +
+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"
diff -r 918687637307 -r 3adc06d6504f src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Algebra/Ideal.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,6 +1,5 @@
 (*
   Title:     HOL/Algebra/CIdeal.thy
-  Id:        $Id$
   Author:    Stephan Hohe, TU Muenchen
 *)
 
@@ -14,11 +13,11 @@
 
 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"
 
-interpretation ideal \<subseteq> abelian_subgroup I R
+sublocale ideal \<subseteq> abelian_subgroup I R
 apply (intro abelian_subgroupI3 abelian_group.intro)
   apply (rule ideal.axioms, rule ideal_axioms)
  apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms)
@@ -37,7 +36,7 @@
       and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
   shows "ideal I R"
 proof -
-  interpret ring [R] by fact
+  interpret ring R by fact
   show ?thesis  apply (intro ideal.intro ideal_axioms.intro additive_subgroupI)
      apply (rule a_subgroup)
     apply (rule is_ring)
@@ -68,7 +67,7 @@
   assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
   shows "principalideal I R"
 proof -
-  interpret ideal [I R] by fact
+  interpret ideal I R by fact
   show ?thesis  by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
 qed
 
@@ -89,7 +88,7 @@
      and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
   shows "maximalideal I R"
 proof -
-  interpret ideal [I R] by fact
+  interpret ideal I R by fact
   show ?thesis by (intro maximalideal.intro maximalideal_axioms.intro)
     (rule is_ideal, rule I_notcarr, rule I_maximal)
 qed
@@ -112,8 +111,8 @@
       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 ideal [I R] by fact
-  interpret cring [R] by fact
+  interpret ideal I R by fact
+  interpret cring R by fact
   show ?thesis by (intro primeideal.intro primeideal_axioms.intro)
     (rule is_ideal, rule is_cring, rule I_notcarr, rule I_prime)
 qed
@@ -128,8 +127,8 @@
       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 cring [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)
     apply (erule (1) I_l_closed)
@@ -207,8 +206,8 @@
   assumes "ideal J R"
   shows "ideal (I \<inter> J) R"
 proof -
-  interpret ideal [I R] by fact
-  interpret ideal [J R] by fact
+  interpret ideal I R by fact
+  interpret ideal J R by fact
   show ?thesis
 apply (intro idealI subgroup.intro)
       apply (rule is_ring)
@@ -245,7 +244,7 @@
   from notempty have "\<exists>I0. I0 \<in> S" by blast
   from this obtain I0 where I0S: "I0 \<in> S" by auto
 
-  interpret ideal ["I0" "R"] by (rule Sideals[OF I0S])
+  interpret ideal I0 R by (rule Sideals[OF I0S])
 
   from xI[OF I0S] have "x \<in> I0" .
   from this and a_subset show "x \<in> carrier R" by fast
@@ -258,13 +257,13 @@
 
   fix J
   assume JS: "J \<in> S"
-  interpret ideal ["J" "R"] by (rule Sideals[OF JS])
+  interpret ideal J R by (rule Sideals[OF JS])
   from xI[OF JS] and yI[OF JS]
       show "x \<oplus> y \<in> J" by (rule a_closed)
 next
   fix J
   assume JS: "J \<in> S"
-  interpret ideal ["J" "R"] by (rule Sideals[OF JS])
+  interpret ideal J R by (rule Sideals[OF JS])
   show "\<zero> \<in> J" by simp
 next
   fix x
@@ -273,7 +272,7 @@
 
   fix J
   assume JS: "J \<in> S"
-  interpret ideal ["J" "R"] by (rule Sideals[OF JS])
+  interpret ideal J R by (rule Sideals[OF JS])
 
   from xI[OF JS]
       show "\<ominus> x \<in> J" by (rule a_inv_closed)
@@ -285,7 +284,7 @@
 
   fix J
   assume JS: "J \<in> S"
-  interpret ideal ["J" "R"] by (rule Sideals[OF JS])
+  interpret ideal J R by (rule Sideals[OF JS])
 
   from xI[OF JS] and ycarr
       show "y \<otimes> x \<in> J" by (rule I_l_closed)
@@ -297,7 +296,7 @@
 
   fix J
   assume JS: "J \<in> S"
-  interpret ideal ["J" "R"] by (rule Sideals[OF JS])
+  interpret ideal J R by (rule Sideals[OF JS])
 
   from xI[OF JS] and ycarr
       show "x \<otimes> y \<in> J" by (rule I_r_closed)
@@ -443,7 +442,7 @@
 lemma (in ring) genideal_one:
   "Idl {\<one>} = carrier R"
 proof -
-  interpret ideal ["Idl {\<one>}" "R"] by (rule genideal_ideal, fast intro: one_closed)
+  interpret ideal "Idl {\<one>}" "R" by (rule genideal_ideal, fast intro: one_closed)
   show "Idl {\<one>} = carrier R"
   apply (rule, rule a_subset)
   apply (simp add: one_imp_carrier genideal_self')
@@ -533,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
@@ -580,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
@@ -660,7 +659,7 @@
   assumes "cring R"
   shows "\<exists>x\<in>I. I = carrier R #> x"
 proof -
-  interpret cring [R] by fact
+  interpret cring R by fact
   from generate
       obtain i
         where icarr: "i \<in> carrier R"
@@ -693,7 +692,7 @@
   assumes notprime: "\<not> primeideal I R"
   shows "carrier R = I \<or> (\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I)"
 proof (rule ccontr, clarsimp)
-  interpret cring [R] by fact
+  interpret cring R by fact
   assume InR: "carrier R \<noteq> I"
      and "\<forall>a. a \<in> carrier R \<longrightarrow> (\<forall>b. a \<otimes> b \<in> I \<longrightarrow> b \<in> carrier R \<longrightarrow> a \<in> I \<or> b \<in> I)"
   hence 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" by simp
@@ -713,7 +712,7 @@
   obtains "carrier R = I"
     | "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I"
 proof -
-  interpret R: cring [R] by fact
+  interpret R!: cring R by fact
   assume "carrier R = I ==> thesis"
     and "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I \<Longrightarrow> thesis"
   then show thesis using primeidealCD [OF R.is_cring notprime] by blast
@@ -726,13 +725,13 @@
 apply (rule domain.intro, rule is_cring)
 apply (rule domain_axioms.intro)
 proof (rule ccontr, simp)
-  interpret primeideal ["{\<zero>}" "R"] by (rule pi)
+  interpret primeideal "{\<zero>}" "R" by (rule pi)
   assume "\<one> = \<zero>"
   hence "carrier R = {\<zero>}" by (rule one_zeroD)
   from this[symmetric] and I_notcarr
       show "False" by simp
 next
-  interpret primeideal ["{\<zero>}" "R"] by (rule pi)
+  interpret primeideal "{\<zero>}" "R" by (rule pi)
   fix a b
   assume ab: "a \<otimes> b = \<zero>"
      and carr: "a \<in> carrier R" "b \<in> carrier R"
@@ -771,7 +770,7 @@
   assumes acarr: "a \<in> carrier R"
   shows "ideal {x\<in>carrier R. a \<otimes> x \<in> I} R"
 proof -
-  interpret cring [R] by fact
+  interpret cring R by fact
   show ?thesis apply (rule idealI)
     apply (rule cring.axioms[OF is_cring])
     apply (rule subgroup.intro)
@@ -812,7 +811,7 @@
   assumes "maximalideal I R"
   shows "primeideal I R"
 proof -
-  interpret maximalideal [I R] by fact
+  interpret maximalideal I R by fact
   show ?thesis apply (rule ccontr)
     apply (rule primeidealCE)
     apply (rule is_cring)
@@ -830,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"
@@ -855,7 +854,7 @@
     have "\<one> \<notin> J" unfolding J_def by fast
     hence Jncarr: "J \<noteq> carrier R" by fast
     
-    interpret ideal ["J" "R"] by (rule idealJ)
+    interpret ideal J R by (rule idealJ)
     
     have "J = I \<or> J = carrier R"
       apply (intro I_maximal)
@@ -932,7 +931,7 @@
   fix I
   assume a: "I \<in> {I. ideal I R}"
   with this
-      interpret ideal ["I" "R"] by simp
+      interpret ideal I R by simp
 
   show "I \<in> {{\<zero>}, carrier R}"
   proof (cases "\<exists>a. a \<in> I - {\<zero>}")
@@ -1019,7 +1018,7 @@
   fix J
   assume Jn0: "J \<noteq> {\<zero>}"
      and idealJ: "ideal J R"
-  interpret ideal ["J" "R"] by (rule idealJ)
+  interpret ideal J R by (rule idealJ)
   have "{\<zero>} \<subseteq> J" by (rule ccontr, simp)
   from zeromax and idealJ and this and a_subset
       have "J = {\<zero>} \<or> J = carrier R" by (rule maximalideal.I_maximal)
diff -r 918687637307 -r 3adc06d6504f src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,6 +1,5 @@
 (*
   Title:     HOL/Algebra/IntRing.thy
-  Id:        $Id$
   Author:    Stephan Hohe, TU Muenchen
 *)
 
@@ -97,7 +96,7 @@
   interpretation needs to be done as early as possible --- that is,
   with as few assumptions as possible. *}
 
-interpretation int: monoid ["\<Z>"]
+interpretation int!: monoid \<Z>
   where "carrier \<Z> = UNIV"
     and "mult \<Z> x y = x * y"
     and "one \<Z> = 1"
@@ -105,7 +104,7 @@
 proof -
   -- "Specification"
   show "monoid \<Z>" proof qed (auto simp: int_ring_def)
-  then interpret int: monoid ["\<Z>"] .
+  then interpret int!: monoid \<Z> .
 
   -- "Carrier"
   show "carrier \<Z> = UNIV" by (simp add: int_ring_def)
@@ -117,12 +116,12 @@
   show "pow \<Z> x n = x^n" by (induct n) (simp, simp add: int_ring_def)+
 qed
 
-interpretation int: comm_monoid ["\<Z>"]
+interpretation int!: comm_monoid \<Z>
   where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
 proof -
   -- "Specification"
   show "comm_monoid \<Z>" proof qed (auto simp: int_ring_def)
-  then interpret int: comm_monoid ["\<Z>"] .
+  then interpret int!: comm_monoid \<Z> .
 
   -- "Operations"
   { fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
@@ -140,14 +139,14 @@
   qed
 qed
 
-interpretation int: abelian_monoid ["\<Z>"]
+interpretation int!: abelian_monoid \<Z>
   where "zero \<Z> = 0"
     and "add \<Z> x y = x + y"
     and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
 proof -
   -- "Specification"
   show "abelian_monoid \<Z>" proof qed (auto simp: int_ring_def)
-  then interpret int: abelian_monoid ["\<Z>"] .
+  then interpret int!: abelian_monoid \<Z> .
 
   -- "Operations"
   { fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) }
@@ -165,7 +164,7 @@
   qed
 qed
 
-interpretation int: abelian_group ["\<Z>"]
+interpretation int!: abelian_group \<Z>
   where "a_inv \<Z> x = - x"
     and "a_minus \<Z> x y = x - y"
 proof -
@@ -175,7 +174,7 @@
     show "!!x. x \<in> carrier \<Z> ==> EX y : carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
       by (simp add: int_ring_def) arith
   qed (auto simp: int_ring_def)
-  then interpret int: abelian_group ["\<Z>"] .
+  then interpret int!: abelian_group \<Z> .
 
   -- "Operations"
   { fix x y have "add \<Z> x y = x + y" by (simp add: int_ring_def) }
@@ -188,7 +187,7 @@
   show "a_minus \<Z> x y = x - y" by (simp add: int.minus_eq add a_inv)
 qed
 
-interpretation int: "domain" ["\<Z>"]
+interpretation int!: "domain" \<Z>
   proof qed (auto simp: int_ring_def left_distrib right_distrib)
 
 
@@ -204,8 +203,8 @@
   "(True ==> PROP R) == PROP R"
   by simp_all
 
-interpretation int (* FIXME [unfolded UNIV] *) :
-  partial_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
+interpretation int! (* FIXME [unfolded UNIV] *) :
+  partial_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
   where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
     and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
     and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
@@ -220,8 +219,8 @@
     by (simp add: lless_def) auto
 qed
 
-interpretation int (* FIXME [unfolded UNIV] *) :
-  lattice ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
+interpretation int! (* FIXME [unfolded UNIV] *) :
+  lattice "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
   where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
     and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
 proof -
@@ -233,7 +232,7 @@
     apply (simp add: greatest_def Lower_def)
     apply arith
     done
-  then interpret int: lattice ["?Z"] .
+  then interpret int!: lattice "?Z" .
   show "join ?Z x y = max x y"
     apply (rule int.joinI)
     apply (simp_all add: least_def Upper_def)
@@ -246,8 +245,8 @@
     done
 qed
 
-interpretation int (* [unfolded UNIV] *) :
-  total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
+interpretation int! (* [unfolded UNIV] *) :
+  total_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
   proof qed clarsimp
 
 
@@ -404,7 +403,7 @@
   assumes zmods: "ZMod m a = ZMod m b"
   shows "a mod m = b mod m"
 proof -
-  interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast)
+  interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> by (rule int.genideal_ideal, fast)
   from zmods
       have "b \<in> ZMod m a"
       unfolding ZMod_def
@@ -428,7 +427,7 @@
 lemma ZMod_mod:
   shows "ZMod m a = ZMod m (a mod m)"
 proof -
-  interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast)
+  interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> by (rule int.genideal_ideal, fast)
   show ?thesis
       unfolding ZMod_def
   apply (rule a_repr_independence'[symmetric])
diff -r 918687637307 -r 3adc06d6504f src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Algebra/Lattice.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,6 +1,5 @@
 (*
   Title:     HOL/Algebra/Lattice.thy
-  Id:        $Id$
   Author:    Clemens Ballarin, started 7 November 2003
   Copyright: Clemens Ballarin
 
@@ -16,7 +15,7 @@
 record 'a gorder = "'a eq_object" +
   le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
 
-locale weak_partial_order = equivalence L +
+locale weak_partial_order = equivalence L for L (structure) +
   assumes le_refl [intro, simp]:
       "x \<in> carrier L ==> x \<sqsubseteq> x"
     and weak_le_anti_sym [intro]:
@@ -920,7 +919,7 @@
 
 text {* Total orders are lattices. *}
 
-interpretation weak_total_order < weak_lattice
+sublocale weak_total_order < weak_lattice
 proof
   fix x y
   assume L: "x \<in> carrier L"  "y \<in> carrier L"
@@ -1126,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})"
 
-interpretation upper_semilattice < weak_upper_semilattice
+sublocale upper_semilattice < 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})"
 
-interpretation lower_semilattice < weak_lower_semilattice
+sublocale lower_semilattice < weak_lower_semilattice
   proof qed (rule inf_of_two_exists)
 
 locale lattice = upper_semilattice + lower_semilattice
@@ -1184,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"
 
-interpretation total_order < weak_total_order
+sublocale total_order < weak_total_order
   proof qed (rule total_order_total)
 
 text {* Introduction rule: the usual definition of total order *}
@@ -1196,7 +1195,7 @@
 
 text {* Total orders are lattices. *}
 
-interpretation total_order < lattice
+sublocale total_order < lattice
   proof qed (auto intro: sup_of_two_exists inf_of_two_exists)
 
 
@@ -1208,7 +1207,7 @@
     and inf_exists:
     "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
 
-interpretation complete_lattice < weak_complete_lattice
+sublocale complete_lattice < weak_complete_lattice
   proof qed (auto intro: sup_exists inf_exists)
 
 text {* Introduction rule: the usual definition of complete lattice *}
diff -r 918687637307 -r 3adc06d6504f src/HOL/Algebra/Module.thy
--- a/src/HOL/Algebra/Module.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Algebra/Module.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Algebra/Module.thy
-    ID:         $Id$
     Author:     Clemens Ballarin, started 15 April 2003
     Copyright:  Clemens Ballarin
 *)
@@ -14,7 +13,7 @@
 record ('a, 'b) module = "'b ring" +
   smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
 
-locale module = cring R + abelian_group M +
+locale module = R: cring + M: abelian_group M for M (structure) +
   assumes smult_closed [simp, intro]:
       "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
     and smult_l_distr:
@@ -29,7 +28,7 @@
     and smult_one [simp]:
       "x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> x = x"
 
-locale algebra = module R M + cring M +
+locale algebra = module + cring M +
   assumes smult_assoc2:
       "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
       (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
diff -r 918687637307 -r 3adc06d6504f src/HOL/Algebra/QuotRing.thy
--- a/src/HOL/Algebra/QuotRing.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Algebra/QuotRing.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,6 +1,5 @@
 (*
   Title:     HOL/Algebra/QuotRing.thy
-  Id:        $Id$
   Author:    Stephan Hohe
 *)
 
@@ -158,7 +157,7 @@
   assumes "cring R"
   shows "cring (R Quot I)"
 proof -
-  interpret cring [R] by fact
+  interpret cring R by fact
   show ?thesis apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro)
   apply (rule quotient_is_ring)
  apply (rule ring.axioms[OF quotient_is_ring])
@@ -173,7 +172,7 @@
   assumes "cring R"
   shows "ring_hom_cring R (R Quot I) (op +> I)"
 proof -
-  interpret cring [R] by fact
+  interpret cring R by fact
   show ?thesis apply (rule ring_hom_cringI)
   apply (rule rcos_ring_hom_ring)
  apply (rule R.is_cring)
@@ -244,7 +243,7 @@
   assumes "cring R"
   shows "field (R Quot I)"
 proof -
-  interpret cring [R] by fact
+  interpret cring R by fact
   show ?thesis apply (intro cring.cring_fieldI2)
   apply (rule quotient_is_cring, rule is_cring)
  defer 1
diff -r 918687637307 -r 3adc06d6504f src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Algebra/Ring.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,6 +1,5 @@
 (*
   Title:     The algebraic hierarchy of rings
-  Id:        $Id$
   Author:    Clemens Ballarin, started 9 December 1996
   Copyright: Clemens Ballarin
 *)
@@ -187,7 +186,7 @@
   assumes cg: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   shows "abelian_group G"
 proof -
-  interpret comm_group ["\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
+  interpret comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
     by (rule cg)
   show "abelian_group G" ..
 qed
@@ -360,7 +359,7 @@
 
 subsection {* Rings: Basic Definitions *}
 
-locale ring = abelian_group R + monoid R +
+locale ring = abelian_group R + monoid R for R (structure) +
   assumes l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
       ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
     and r_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
@@ -585,8 +584,8 @@
   assumes RS: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier S" "d \<in> carrier S"
   shows "a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^bsub>S\<^esub> d = d \<otimes>\<^bsub>S\<^esub> c"
 proof -
-  interpret ring [R] by fact
-  interpret cring [S] by fact
+  interpret ring R by fact
+  interpret cring S by fact
 ML_val {* Algebra.print_structures @{context} *}
   from RS show ?thesis by algebra
 qed
@@ -597,7 +596,7 @@
   assumes R: "a \<in> carrier R" "b \<in> carrier R"
   shows "a \<ominus> (a \<ominus> b) = b"
 proof -
-  interpret ring [R] by fact
+  interpret ring R by fact
   from R show ?thesis by algebra
 qed
 
@@ -771,7 +770,8 @@
   shows "h \<in> ring_hom R S ==> h \<one> = \<one>\<^bsub>S\<^esub>"
   by (simp add: ring_hom_def)
 
-locale ring_hom_cring = cring R + cring S +
+locale ring_hom_cring = R: cring R + S: cring S
+    for R (structure) and S (structure) +
   fixes h
   assumes homh [simp, intro]: "h \<in> ring_hom R S"
   notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
diff -r 918687637307 -r 3adc06d6504f src/HOL/Algebra/RingHom.thy
--- a/src/HOL/Algebra/RingHom.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Algebra/RingHom.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,6 +1,5 @@
 (*
   Title:     HOL/Algebra/RingHom.thy
-  Id:        $Id$
   Author:    Stephan Hohe, TU Muenchen
 *)
 
@@ -11,15 +10,17 @@
 section {* Homomorphisms of Non-Commutative Rings *}
 
 text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
-locale ring_hom_ring = ring R + ring S + var h +
+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]
 
-interpretation ring_hom_cring \<subseteq> ring_hom_ring
+sublocale ring_hom_cring \<subseteq> ring_hom_ring
   proof qed (rule homh)
 
-interpretation ring_hom_ring \<subseteq> abelian_group_hom R S
+sublocale ring_hom_ring \<subseteq> abelian_group_hom R S
 apply (rule abelian_group_homI)
   apply (rule R.is_abelian_group)
  apply (rule S.is_abelian_group)
@@ -44,8 +45,8 @@
       and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
   shows "ring_hom_ring R S h"
 proof -
-  interpret ring [R] by fact
-  interpret ring [S] by fact
+  interpret ring R by fact
+  interpret ring S by fact
   show ?thesis apply unfold_locales
 apply (unfold ring_hom_def, safe)
    apply (simp add: hom_closed Pi_def)
@@ -60,8 +61,8 @@
   assumes h: "h \<in> ring_hom R S"
   shows "ring_hom_ring R S h"
 proof -
-  interpret R: ring [R] by fact
-  interpret S: ring [S] by fact
+  interpret R!: ring R by fact
+  interpret S!: ring S by fact
   show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
     apply (rule R.is_ring)
     apply (rule S.is_ring)
@@ -76,9 +77,9 @@
       and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
   shows "ring_hom_ring R S h"
 proof -
-  interpret abelian_group_hom [R S h] by fact
-  interpret R: ring [R] by fact
-  interpret S: ring [S] by fact
+  interpret abelian_group_hom R S h by fact
+  interpret R!: ring R by fact
+  interpret S!: ring S by fact
   show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
     apply (insert group_hom.homh[OF a_group_hom])
     apply (unfold hom_def ring_hom_def, simp)
@@ -92,9 +93,9 @@
   assumes "ring_hom_ring R S h" "cring R" "cring S"
   shows "ring_hom_cring R S h"
 proof -
-  interpret ring_hom_ring [R S h] by fact
-  interpret R: cring [R] by fact
-  interpret S: cring [S] by fact
+  interpret ring_hom_ring R S h by fact
+  interpret R!: cring R by fact
+  interpret S!: cring S by fact
   show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
     (rule R.is_cring, rule S.is_cring, rule homh)
 qed
@@ -124,7 +125,7 @@
       and xrcos: "x \<in> a_kernel R S h +> a"
   shows "h x = h a"
 proof -
-  interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
+  interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
 
   from xrcos
       have "\<exists>i \<in> a_kernel R S h. x = i \<oplus> a" by (simp add: a_r_coset_defs)
@@ -152,7 +153,7 @@
       and hx: "h x = h a"
   shows "x \<in> a_kernel R S h +> a"
 proof -
-  interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
+  interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
  
   note carr = acarr xcarr
   note hcarr = acarr[THEN hom_closed] xcarr[THEN hom_closed]
@@ -180,7 +181,7 @@
 apply rule defer 1
 apply clarsimp defer 1
 proof
-  interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
+  interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
 
   fix x
   assume xrcos: "x \<in> a_kernel R S h +> a"
@@ -193,7 +194,7 @@
   from xcarr and this
       show "x \<in> {x \<in> carrier R. h x = h a}" by fast
 next
-  interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
+  interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
 
   fix x
   assume xcarr: "x \<in> carrier R"
diff -r 918687637307 -r 3adc06d6504f src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,6 +1,5 @@
 (*
   Title:     HOL/Algebra/UnivPoly.thy
-  Id:        $Id$
   Author:    Clemens Ballarin, started 9 December 1996
   Copyright: Clemens Ballarin
 
@@ -176,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
 
-interpretation UP_cring < UP_ring
-  by (rule P_def) intro_locales
+sublocale UP_cring < UP_ring
+  by intro_locales [1] (rule P_def)
 
-locale UP_domain = UP + "domain" R
+locale UP_domain = UP + R: "domain" R
 
-interpretation UP_domain < UP_cring
-  by (rule P_def) intro_locales
+sublocale UP_domain < UP_cring
+  by intro_locales [1] (rule P_def)
 
 context UP
 begin
@@ -458,8 +457,8 @@
 
 end
 
-interpretation UP_ring < ring P using UP_ring .
-interpretation 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 *}
@@ -508,7 +507,7 @@
   "algebra R P" by (auto intro!: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr
     UP_smult_assoc1 UP_smult_assoc2)
 
-interpretation UP_cring < algebra R P using UP_algebra .
+sublocale UP_cring < algebra R P using UP_algebra .
 
 
 subsection {* Further Lemmas Involving Monomials *}
@@ -1085,7 +1084,7 @@
   Interpretation of theorems from @{term domain}.
 *}
 
-interpretation UP_domain < "domain" P
+sublocale UP_domain < "domain" P
   by intro_locales (rule domain.axioms UP_domain)+
 
 
@@ -1204,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
@@ -1350,7 +1351,7 @@
 
 text {* Interpretation of ring homomorphism lemmas. *}
 
-interpretation UP_univ_prop < ring_hom_cring P S Eval
+sublocale UP_univ_prop < ring_hom_cring P S Eval
   apply (unfold Eval_def)
   apply intro_locales
   apply (rule ring_hom_cring.axioms)
@@ -1391,7 +1392,7 @@
   assumes R: "r \<in> carrier R" and S: "s \<in> carrier S"
   shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
 proof -
-  interpret UP_univ_prop [R S h P s _]
+  interpret UP_univ_prop R S h P s "eval R S h s"
     using UP_pre_univ_prop_axioms P_def R S
     by (auto intro: UP_univ_prop.intro UP_univ_prop_axioms.intro)
   from R
@@ -1428,8 +1429,8 @@
     and P: "p \<in> carrier P" and S: "s \<in> carrier S"
   shows "Phi p = Psi p"
 proof -
-  interpret ring_hom_cring [P S Phi] by fact
-  interpret ring_hom_cring [P S Psi] by fact
+  interpret ring_hom_cring P S Phi by fact
+  interpret ring_hom_cring P S Psi by fact
   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 monom_mult [THEN sym] monom_pow del: monom_mult)
@@ -1772,9 +1773,9 @@
   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 P 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)
+  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" 
     and mon0_closed: "monom P a 0 \<in> carrier P" 
     and min_mon0_closed: "\<ominus>\<^bsub>P\<^esub> monom P a 0 \<in> carrier P"
@@ -1819,7 +1820,7 @@
     and deg_r_0: "deg R r = 0"
     shows "r = monom P (eval R R id a f) 0"
 proof -
-  interpret UP_pre_univ_prop [R R id P] proof qed simp
+  interpret UP_pre_univ_prop R R id P 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
   have "eval R R id a f = eval R R id a ?gq \<oplus>\<^bsub>R\<^esub> eval R R id a r"
@@ -1885,7 +1886,7 @@
   "UP INTEG"} globally.
 *}
 
-interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id]
+interpretation INTEG!: UP_pre_univ_prop INTEG INTEG id
   using INTEG_id_eval by simp_all
 
 lemma INTEG_closed [intro, simp]:
diff -r 918687637307 -r 3adc06d6504f src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Complex.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -345,13 +345,13 @@
 
 subsection {* Completeness of the Complexes *}
 
-interpretation Re: bounded_linear ["Re"]
+interpretation Re!: bounded_linear "Re"
 apply (unfold_locales, simp, simp)
 apply (rule_tac x=1 in exI)
 apply (simp add: complex_norm_def)
 done
 
-interpretation Im: bounded_linear ["Im"]
+interpretation Im!: bounded_linear "Im"
 apply (unfold_locales, simp, simp)
 apply (rule_tac x=1 in exI)
 apply (simp add: complex_norm_def)
@@ -513,7 +513,7 @@
 lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>"
 by (simp add: norm_mult power2_eq_square)
 
-interpretation cnj: bounded_linear ["cnj"]
+interpretation cnj!: bounded_linear "cnj"
 apply (unfold_locales)
 apply (rule complex_cnj_add)
 apply (rule complex_cnj_scaleR)
diff -r 918687637307 -r 3adc06d6504f src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Divides.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -639,7 +639,7 @@
 
 text {* @{term "op dvd"} is a partial order *}
 
-interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"]
+class_interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"]
   proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
 
 lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
diff -r 918687637307 -r 3adc06d6504f src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -750,7 +750,7 @@
 assumes "finite A" and "a \<notin> A"
 shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"
 proof -
-  interpret I: fun_left_comm ["%x y. (g x) * y"]
+  interpret I: fun_left_comm "%x y. (g x) * y"
     by unfold_locales (simp add: mult_ac)
   show ?thesis using assms by(simp add:fold_image_def I.fold_insert)
 qed
@@ -798,7 +798,7 @@
     and hyp: "\<And>x y. h (g x y) = times x (h y)"
   shows "h (fold g j w A) = fold times j (h w) A"
 proof -
-  interpret ab_semigroup_mult [g] by fact
+  class_interpret ab_semigroup_mult [g] by fact
   show ?thesis using fin hyp by (induct set: finite) simp_all
 qed
 *)
@@ -873,7 +873,7 @@
 
 subsection {* Generalized summation over a set *}
 
-interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"]
+class_interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"]
   proof qed (auto intro: add_assoc add_commute)
 
 definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
@@ -1760,7 +1760,7 @@
 proof (induct rule: finite_induct)
   case empty then show ?case by simp
 next
-  interpret ab_semigroup_mult ["op Un"]
+  class_interpret ab_semigroup_mult ["op Un"]
     proof qed auto
   case insert 
   then show ?case by simp
@@ -1943,7 +1943,7 @@
 assumes fold: "fold_graph times (b::'a) A y" and "b \<notin> A"
 shows "fold_graph times z (insert b A) (z * y)"
 proof -
-  interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
+  interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
 from assms show ?thesis
 proof (induct rule: fold_graph.induct)
   case emptyI thus ?case by (force simp add: fold_insert_aux mult_commute)
@@ -1983,7 +1983,7 @@
 lemma fold1_eq_fold:
 assumes "finite A" "a \<notin> A" shows "fold1 times (insert a A) = fold times a A"
 proof -
-  interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
+  interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
   from assms show ?thesis
 apply (simp add: fold1_def fold_def)
 apply (rule the_equality)
@@ -2010,7 +2010,7 @@
   assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
   shows "fold1 times (insert x A) = x * fold1 times A"
 proof -
-  interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
+  interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
   from nonempty obtain a A' where "A = insert a A' & a ~: A'"
     by (auto simp add: nonempty_iff)
   with A show ?thesis
@@ -2033,7 +2033,7 @@
   assumes nonempty: "A \<noteq> {}" and A: "finite A" 
   shows "fold1 times (insert x A) = x * fold1 times A"
 proof -
-  interpret fun_left_comm_idem ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"]
+  interpret fun_left_comm_idem "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"
     by (rule fun_left_comm_idem)
   from nonempty obtain a A' where A': "A = insert a A' & a ~: A'"
     by (auto simp add: nonempty_iff)
@@ -2198,7 +2198,7 @@
   assumes "finite A" "A \<noteq> {}"
   shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
 proof -
-  interpret ab_semigroup_idem_mult [inf]
+  class_interpret ab_semigroup_idem_mult [inf]
     by (rule ab_semigroup_idem_mult_inf)
   show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
 qed
@@ -2213,7 +2213,7 @@
   proof (induct rule: finite_ne_induct)
     case singleton thus ?case by simp
   next
-    interpret ab_semigroup_idem_mult [inf]
+    class_interpret ab_semigroup_idem_mult [inf]
       by (rule ab_semigroup_idem_mult_inf)
     case (insert x F)
     from insert(5) have "a = x \<or> a \<in> F" by simp
@@ -2288,7 +2288,7 @@
     and "A \<noteq> {}"
   shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
 proof -
-  interpret ab_semigroup_idem_mult [inf]
+  class_interpret ab_semigroup_idem_mult [inf]
     by (rule ab_semigroup_idem_mult_inf)
   from assms show ?thesis
     by (simp add: Inf_fin_def image_def
@@ -2303,7 +2303,7 @@
   case singleton thus ?case
     by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
 next
-  interpret ab_semigroup_idem_mult [inf]
+  class_interpret ab_semigroup_idem_mult [inf]
     by (rule ab_semigroup_idem_mult_inf)
   case (insert x A)
   have finB: "finite {sup x b |b. b \<in> B}"
@@ -2333,7 +2333,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
 proof -
-  interpret ab_semigroup_idem_mult [sup]
+  class_interpret ab_semigroup_idem_mult [sup]
     by (rule ab_semigroup_idem_mult_sup)
   from assms show ?thesis
     by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
@@ -2357,7 +2357,7 @@
     thus ?thesis by(simp add: insert(1) B(1))
   qed
   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
-  interpret ab_semigroup_idem_mult [sup]
+  class_interpret ab_semigroup_idem_mult [sup]
     by (rule ab_semigroup_idem_mult_sup)
   have "inf (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^bsub>fin\<^esub>B)"
     using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
@@ -2386,7 +2386,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
 proof -
-  interpret ab_semigroup_idem_mult [inf]
+  class_interpret ab_semigroup_idem_mult [inf]
     by (rule ab_semigroup_idem_mult_inf)
   from assms show ?thesis
   unfolding Inf_fin_def by (induct A set: finite)
@@ -2397,7 +2397,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
 proof -
-  interpret ab_semigroup_idem_mult [sup]
+  class_interpret ab_semigroup_idem_mult [sup]
     by (rule ab_semigroup_idem_mult_sup)
   from assms show ?thesis
   unfolding Sup_fin_def by (induct A set: finite)
@@ -2446,7 +2446,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
 proof -
-  interpret ab_semigroup_idem_mult [min]
+  class_interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms show ?thesis
   by (induct rule: finite_ne_induct)
@@ -2457,7 +2457,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
 proof -
-  interpret ab_semigroup_idem_mult [min]
+  class_interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms show ?thesis
   by (induct rule: finite_ne_induct)
@@ -2468,7 +2468,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
 proof -
-  interpret ab_semigroup_idem_mult [min]
+  class_interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms show ?thesis
   by (induct rule: finite_ne_induct)
@@ -2481,7 +2481,7 @@
 proof cases
   assume "A = B" thus ?thesis by simp
 next
-  interpret ab_semigroup_idem_mult [min]
+  class_interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   assume "A \<noteq> B"
   have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
@@ -2515,7 +2515,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Min (insert x A) = min x (Min A)"
 proof -
-  interpret ab_semigroup_idem_mult [min]
+  class_interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
 qed
@@ -2524,7 +2524,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Max (insert x A) = max x (Max A)"
 proof -
-  interpret ab_semigroup_idem_mult [max]
+  class_interpret ab_semigroup_idem_mult [max]
     by (rule ab_semigroup_idem_mult_max)
   from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
 qed
@@ -2533,7 +2533,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Min A \<in> A"
 proof -
-  interpret ab_semigroup_idem_mult [min]
+  class_interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
 qed
@@ -2542,7 +2542,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Max A \<in> A"
 proof -
-  interpret ab_semigroup_idem_mult [max]
+  class_interpret ab_semigroup_idem_mult [max]
     by (rule ab_semigroup_idem_mult_max)
   from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
 qed
@@ -2551,7 +2551,7 @@
   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
   shows "Min (A \<union> B) = min (Min A) (Min B)"
 proof -
-  interpret ab_semigroup_idem_mult [min]
+  class_interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms show ?thesis
     by (simp add: Min_def fold1_Un2)
@@ -2561,7 +2561,7 @@
   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
   shows "Max (A \<union> B) = max (Max A) (Max B)"
 proof -
-  interpret ab_semigroup_idem_mult [max]
+  class_interpret ab_semigroup_idem_mult [max]
     by (rule ab_semigroup_idem_mult_max)
   from assms show ?thesis
     by (simp add: Max_def fold1_Un2)
@@ -2572,7 +2572,7 @@
     and "finite N" and "N \<noteq> {}"
   shows "h (Min N) = Min (h ` N)"
 proof -
-  interpret ab_semigroup_idem_mult [min]
+  class_interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms show ?thesis
     by (simp add: Min_def hom_fold1_commute)
@@ -2583,7 +2583,7 @@
     and "finite N" and "N \<noteq> {}"
   shows "h (Max N) = Max (h ` N)"
 proof -
-  interpret ab_semigroup_idem_mult [max]
+  class_interpret ab_semigroup_idem_mult [max]
     by (rule ab_semigroup_idem_mult_max)
   from assms show ?thesis
     by (simp add: Max_def hom_fold1_commute [of h])
@@ -2593,7 +2593,7 @@
   assumes "finite A" and "x \<in> A"
   shows "Min A \<le> x"
 proof -
-  interpret lower_semilattice ["op \<le>" "op <" min]
+  class_interpret lower_semilattice ["op \<le>" "op <" min]
     by (rule min_lattice)
   from assms show ?thesis by (simp add: Min_def fold1_belowI)
 qed
@@ -2611,7 +2611,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
 proof -
-  interpret lower_semilattice ["op \<le>" "op <" min]
+  class_interpret lower_semilattice ["op \<le>" "op <" min]
     by (rule min_lattice)
   from assms show ?thesis by (simp add: Min_def below_fold1_iff)
 qed
@@ -2629,7 +2629,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
 proof -
-  interpret lower_semilattice ["op \<le>" "op <" min]
+  class_interpret lower_semilattice ["op \<le>" "op <" min]
     by (rule min_lattice)
   from assms show ?thesis by (simp add: Min_def strict_below_fold1_iff)
 qed
@@ -2639,7 +2639,7 @@
   shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
 proof -
   note Max = Max_def
-  interpret linorder ["op \<ge>" "op >"]
+  class_interpret linorder ["op \<ge>" "op >"]
     by (rule dual_linorder)
   from assms show ?thesis
     by (simp add: Max strict_below_fold1_iff [folded dual_max])
@@ -2649,7 +2649,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
 proof -
-  interpret lower_semilattice ["op \<le>" "op <" min]
+  class_interpret lower_semilattice ["op \<le>" "op <" min]
     by (rule min_lattice)
   from assms show ?thesis
     by (simp add: Min_def fold1_below_iff)
@@ -2660,7 +2660,7 @@
   shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
 proof -
   note Max = Max_def
-  interpret linorder ["op \<ge>" "op >"]
+  class_interpret linorder ["op \<ge>" "op >"]
     by (rule dual_linorder)
   from assms show ?thesis
     by (simp add: Max fold1_below_iff [folded dual_max])
@@ -2670,7 +2670,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
 proof -
-  interpret lower_semilattice ["op \<le>" "op <" min]
+  class_interpret lower_semilattice ["op \<le>" "op <" min]
     by (rule min_lattice)
   from assms show ?thesis
     by (simp add: Min_def fold1_strict_below_iff)
@@ -2681,7 +2681,7 @@
   shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
 proof -
   note Max = Max_def
-  interpret linorder ["op \<ge>" "op >"]
+  class_interpret linorder ["op \<ge>" "op >"]
     by (rule dual_linorder)
   from assms show ?thesis
     by (simp add: Max fold1_strict_below_iff [folded dual_max])
@@ -2691,7 +2691,7 @@
   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   shows "Min N \<le> Min M"
 proof -
-  interpret distrib_lattice ["op \<le>" "op <" min max]
+  class_interpret distrib_lattice ["op \<le>" "op <" min max]
     by (rule distrib_lattice_min_max)
   from assms show ?thesis by (simp add: Min_def fold1_antimono)
 qed
@@ -2701,7 +2701,7 @@
   shows "Max M \<le> Max N"
 proof -
   note Max = Max_def
-  interpret linorder ["op \<ge>" "op >"]
+  class_interpret linorder ["op \<ge>" "op >"]
     by (rule dual_linorder)
   from assms show ?thesis
     by (simp add: Max fold1_antimono [folded dual_max])
diff -r 918687637307 -r 3adc06d6504f src/HOL/FrechetDeriv.thy
--- a/src/HOL/FrechetDeriv.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/FrechetDeriv.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -65,8 +65,8 @@
   assumes "bounded_linear g"
   shows "bounded_linear (\<lambda>x. f x + g x)"
 proof -
-  interpret f: bounded_linear [f] by fact
-  interpret g: bounded_linear [g] by fact
+  interpret f: bounded_linear f by fact
+  interpret g: bounded_linear g by fact
   show ?thesis apply (unfold_locales)
     apply (simp only: f.add g.add add_ac)
     apply (simp only: f.scaleR g.scaleR scaleR_right_distrib)
@@ -124,7 +124,7 @@
   assumes "bounded_linear f"
   shows "bounded_linear (\<lambda>x. - f x)"
 proof -
-  interpret f: bounded_linear [f] by fact
+  interpret f: bounded_linear f by fact
   show ?thesis apply (unfold_locales)
     apply (simp add: f.add)
     apply (simp add: f.scaleR)
@@ -151,7 +151,7 @@
   assumes f: "FDERIV f x :> F"
   shows "isCont f x"
 proof -
-  from f interpret F: bounded_linear ["F"] by (rule FDERIV_bounded_linear)
+  from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear)
   have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
     by (rule FDERIV_D [OF f])
   hence "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h * norm h) -- 0 --> 0"
@@ -180,8 +180,8 @@
   assumes "bounded_linear g"
   shows "bounded_linear (\<lambda>x. f (g x))"
 proof -
-  interpret f: bounded_linear [f] by fact
-  interpret g: bounded_linear [g] by fact
+  interpret f: bounded_linear f by fact
+  interpret g: bounded_linear g by fact
   show ?thesis proof (unfold_locales)
     fix x y show "f (g (x + y)) = f (g x) + f (g y)"
       by (simp only: f.add g.add)
@@ -223,8 +223,8 @@
   let ?k = "\<lambda>h. f (x + h) - f x"
   let ?Nf = "\<lambda>h. norm (?Rf h) / norm h"
   let ?Ng = "\<lambda>h. norm (?Rg (?k h)) / norm (?k h)"
-  from f interpret F: bounded_linear ["F"] by (rule FDERIV_bounded_linear)
-  from g interpret G: bounded_linear ["G"] by (rule FDERIV_bounded_linear)
+  from f interpret F!: bounded_linear "F" by (rule FDERIV_bounded_linear)
+  from g interpret G!: bounded_linear "G" by (rule FDERIV_bounded_linear)
   from F.bounded obtain kF where kF: "\<And>x. norm (F x) \<le> norm x * kF" by fast
   from G.bounded obtain kG where kG: "\<And>x. norm (G x) \<le> norm x * kG" by fast
 
@@ -375,9 +375,9 @@
     by (simp only: FDERIV_lemma)
 qed
 
-lemmas FDERIV_mult = bounded_bilinear_locale.mult.prod.FDERIV
+lemmas FDERIV_mult = mult.FDERIV
 
-lemmas FDERIV_scaleR = bounded_bilinear_locale.scaleR.prod.FDERIV
+lemmas FDERIV_scaleR = scaleR.FDERIV
 
 
 subsection {* Powers *}
@@ -409,10 +409,10 @@
 by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
 
 lemmas bounded_linear_mult_const =
-  bounded_bilinear_locale.mult.prod.bounded_linear_left [THEN bounded_linear_compose]
+  mult.bounded_linear_left [THEN bounded_linear_compose]
 
 lemmas bounded_linear_const_mult =
-  bounded_bilinear_locale.mult.prod.bounded_linear_right [THEN bounded_linear_compose]
+  mult.bounded_linear_right [THEN bounded_linear_compose]
 
 lemma FDERIV_inverse:
   fixes x :: "'a::real_normed_div_algebra"
@@ -492,7 +492,7 @@
   fixes x :: "'a::real_normed_field" shows
   "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
  apply (unfold fderiv_def)
- apply (simp add: bounded_bilinear_locale.mult.prod.bounded_linear_left)
+ apply (simp add: mult.bounded_linear_left)
  apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
  apply (subst diff_divide_distrib)
  apply (subst times_divide_eq_left [symmetric])
diff -r 918687637307 -r 3adc06d6504f src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Groebner_Basis.thy
-    ID:         $Id$
     Author:     Amine Chaieb, TU Muenchen
 *)
 
@@ -164,8 +163,8 @@
 
 end
 
-interpretation class_semiring: gb_semiring
-    ["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"]
+interpretation class_semiring!: gb_semiring
+    "op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"
   proof qed (auto simp add: ring_simps power_Suc)
 
 lemmas nat_arith =
@@ -243,8 +242,8 @@
 end
 
 
-interpretation class_ring: gb_ring ["op +" "op *" "op ^"
-    "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"]
+interpretation class_ring!: gb_ring "op +" "op *" "op ^"
+    "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"
   proof qed simp_all
 
 
@@ -344,8 +343,8 @@
   thus "b = 0" by blast
 qed
 
-interpretation class_ringb: ringb
-  ["op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"]
+interpretation class_ringb!: ringb
+  "op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"
 proof(unfold_locales, simp add: ring_simps power_Suc, auto)
   fix w x y z ::"'a::{idom,recpower,number_ring}"
   assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
@@ -360,8 +359,8 @@
 
 declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *}
 
-interpretation natgb: semiringb
-  ["op +" "op *" "op ^" "0::nat" "1"]
+interpretation natgb!: semiringb
+  "op +" "op *" "op ^" "0::nat" "1"
 proof (unfold_locales, simp add: ring_simps power_Suc)
   fix w x y z ::"nat"
   { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
@@ -465,8 +464,8 @@
 
 subsection{* Groebner Bases for fields *}
 
-interpretation class_fieldgb:
-  fieldgb["op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse"] apply (unfold_locales) by (simp_all add: divide_inverse)
+interpretation class_fieldgb!:
+  fieldgb "op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
 
 lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
 lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0"
diff -r 918687637307 -r 3adc06d6504f src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Lattices.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -300,7 +300,7 @@
   by auto
 qed (auto simp add: min_def max_def not_le less_imp_le)
 
-interpretation min_max:
+class_interpretation min_max:
   distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max]
   by (rule distrib_lattice_min_max)
 
diff -r 918687637307 -r 3adc06d6504f src/HOL/Library/Dense_Linear_Order.thy
--- a/src/HOL/Library/Dense_Linear_Order.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Library/Dense_Linear_Order.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*
-    ID:         $Id$
     Author:     Amine Chaieb, TU Muenchen
 *)
 
@@ -304,7 +303,7 @@
 
 text {* Linear order without upper bounds *}
 
-locale linorder_stupid_syntax = linorder
+class_locale linorder_stupid_syntax = linorder
 begin
 notation
   less_eq  ("op \<sqsubseteq>") and
@@ -314,7 +313,7 @@
 
 end
 
-locale linorder_no_ub = linorder_stupid_syntax +
+class_locale linorder_no_ub = linorder_stupid_syntax +
   assumes gt_ex: "\<exists>y. less x y"
 begin
 lemma ge_ex: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto
@@ -363,7 +362,7 @@
 
 text {* Linear order without upper bounds *}
 
-locale linorder_no_lb = linorder_stupid_syntax +
+class_locale linorder_no_lb = linorder_stupid_syntax +
   assumes lt_ex: "\<exists>y. less y x"
 begin
 lemma le_ex: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto
@@ -410,12 +409,12 @@
 end
 
 
-locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
+class_locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
   fixes between
   assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y"
      and  between_same: "between x x = x"
 
-interpretation  constr_dense_linear_order < dense_linear_order 
+class_interpretation  constr_dense_linear_order < dense_linear_order 
   apply unfold_locales
   using gt_ex lt_ex between_less
     by (auto, rule_tac x="between x y" in exI, simp)
@@ -638,7 +637,7 @@
   using eq_diff_eq[where a= x and b=t and c=0] by simp
 
 
-interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order
+class_interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order
  ["op <=" "op <"
    "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"]
 proof (unfold_locales, dlo, dlo, auto)
diff -r 918687637307 -r 3adc06d6504f src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1080,15 +1080,15 @@
 apply simp
 done
 
-interpretation mset_order: order ["op \<le>#" "op <#"]
+class_interpretation mset_order: order ["op \<le>#" "op <#"]
 proof qed (auto intro: order.intro mset_le_refl mset_le_antisym
   mset_le_trans simp: mset_less_def)
 
-interpretation mset_order_cancel_semigroup:
+class_interpretation mset_order_cancel_semigroup:
   pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"]
 proof qed (erule mset_le_mono_add [OF mset_le_refl])
 
-interpretation mset_order_semigroup_cancel:
+class_interpretation mset_order_semigroup_cancel:
   pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"]
 proof qed simp
 
@@ -1404,7 +1404,7 @@
   assumes "left_commutative g"
   shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P")
 proof -
-  interpret left_commutative [g] by fact
+  interpret left_commutative g by fact
   show "PROP ?P" by (induct A) auto
 qed
 
@@ -1436,7 +1436,7 @@
 definition [code del]:
  "image_mset f = fold_mset (op + o single o f) {#}"
 
-interpretation image_left_comm: left_commutative ["op + o single o f"]
+interpretation image_left_comm!: left_commutative "op + o single o f"
   proof qed (simp add:union_ac)
 
 lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
diff -r 918687637307 -r 3adc06d6504f src/HOL/Library/SetsAndFunctions.thy
--- a/src/HOL/Library/SetsAndFunctions.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Library/SetsAndFunctions.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Library/SetsAndFunctions.thy
-    ID:         $Id$
     Author:     Jeremy Avigad and Kevin Donnelly
 *)
 
@@ -108,26 +107,26 @@
   apply simp
   done
 
-interpretation set_semigroup_add: semigroup_add ["op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"]
+class_interpretation set_semigroup_add: semigroup_add ["op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"]
   apply default
   apply (unfold set_plus_def)
   apply (force simp add: add_assoc)
   done
 
-interpretation set_semigroup_mult: semigroup_mult ["op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"]
+class_interpretation set_semigroup_mult: semigroup_mult ["op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"]
   apply default
   apply (unfold set_times_def)
   apply (force simp add: mult_assoc)
   done
 
-interpretation set_comm_monoid_add: comm_monoid_add ["{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"]
+class_interpretation set_comm_monoid_add: comm_monoid_add ["{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"]
   apply default
    apply (unfold set_plus_def)
    apply (force simp add: add_ac)
   apply force
   done
 
-interpretation set_comm_monoid_mult: comm_monoid_mult ["{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"]
+class_interpretation set_comm_monoid_mult: comm_monoid_mult ["{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"]
   apply default
    apply (unfold set_times_def)
    apply (force simp add: mult_ac)
diff -r 918687637307 -r 3adc06d6504f src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/List.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -548,9 +548,9 @@
 lemma append_Nil2 [simp]: "xs @ [] = xs"
 by (induct xs) auto
 
-interpretation semigroup_append: semigroup_add ["op @"]
+class_interpretation semigroup_append: semigroup_add ["op @"]
   proof qed simp
-interpretation monoid_append: monoid_add ["[]" "op @"]
+class_interpretation monoid_append: monoid_add ["[]" "op @"]
   proof qed simp+
 
 lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
diff -r 918687637307 -r 3adc06d6504f src/HOL/MicroJava/BV/Kildall.thy
--- a/src/HOL/MicroJava/BV/Kildall.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -321,7 +321,7 @@
   ss <[r] merges f qs ss \<or> 
   merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un (w-{p}) < w" (is "PROP ?P")
 proof -
-  interpret Semilat [A r f] using assms by (rule Semilat.intro)
+  interpret Semilat A r f using assms by (rule Semilat.intro)
   show "PROP ?P" apply(insert semilat)
     apply (unfold lesssub_def)
     apply (simp (no_asm_simp) add: merges_incr)
@@ -351,7 +351,7 @@
    (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss' <=[r] ts)"
   (is "PROP ?P")
 proof -
-  interpret Semilat [A r f] using assms by (rule Semilat.intro)
+  interpret Semilat A r f using assms by (rule Semilat.intro)
   show "PROP ?P" apply(insert semilat)
 apply (unfold iter_def stables_def)
 apply (rule_tac P = "%(ss,w).
@@ -457,7 +457,7 @@
                  kildall r f step ss0 <=[r] ts)"
   (is "PROP ?P")
 proof -
-  interpret Semilat [A r f] using assms by (rule Semilat.intro)
+  interpret Semilat A r f using assms by (rule Semilat.intro)
   show "PROP ?P"
 apply (unfold kildall_def)
 apply(case_tac "iter f step ss0 (unstables r step ss0)")
@@ -474,7 +474,7 @@
   \<Longrightarrow> is_bcv r T step n A (kildall r f step)"
   (is "PROP ?P")
 proof -
-  interpret Semilat [A r f] using assms by (rule Semilat.intro)
+  interpret Semilat A r f using assms by (rule Semilat.intro)
   show "PROP ?P"
 apply(unfold is_bcv_def wt_step_def)
 apply(insert semilat kildall_properties[of A])
diff -r 918687637307 -r 3adc06d6504f src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -197,7 +197,7 @@
   have "merge c pc ?step (c!Suc pc) =
     (if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'
     then map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc
-    else \<top>)" unfolding merge_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms])
+    else \<top>)" unfolding mrg_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms])
   moreover {
     fix pc' s' assume s': "(pc', s') \<in> set ?step" and suc_pc: "pc' \<noteq> pc+1"
     with less have "s' <=_r \<phi>!pc'" by auto
diff -r 918687637307 -r 3adc06d6504f src/HOL/MicroJava/BV/Listn.thy
--- a/src/HOL/MicroJava/BV/Listn.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/MicroJava/BV/Listn.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -380,7 +380,7 @@
 lemma Listn_sl_aux:
 assumes "semilat (A, r, f)" shows "semilat (Listn.sl n (A,r,f))"
 proof -
-  interpret Semilat [A r f] using assms by (rule Semilat.intro)
+  interpret Semilat A r f using assms by (rule Semilat.intro)
 show ?thesis
 apply (unfold Listn.sl_def)
 apply (simp (no_asm) only: semilat_Def split_conv)
diff -r 918687637307 -r 3adc06d6504f src/HOL/MicroJava/BV/SemilatAlg.thy
--- a/src/HOL/MicroJava/BV/SemilatAlg.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/MicroJava/BV/SemilatAlg.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -67,7 +67,7 @@
 lemma plusplus_closed: assumes "semilat (A, r, f)" shows
   "\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> x ++_f y \<in> A" (is "PROP ?P")
 proof -
-  interpret Semilat [A r f] using assms by (rule Semilat.intro)
+  interpret Semilat A r f using assms by (rule Semilat.intro)
   show "PROP ?P" proof (induct x)
     show "\<And>y. y \<in> A \<Longrightarrow> [] ++_f y \<in> A" by simp
     fix y x xs
@@ -164,7 +164,7 @@
   shows "\<lbrakk>\<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk> 
   \<Longrightarrow> b <=_r map snd [(p', t')\<leftarrow>S. p' = a] ++_f y" 
 proof -
-  interpret Semilat [A r f] using assms by (rule Semilat.intro)
+  interpret Semilat A r f using assms by (rule Semilat.intro)
 
   let "b <=_r ?map ++_f y" = ?thesis
 
diff -r 918687637307 -r 3adc06d6504f src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/NSA/StarDef.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -23,7 +23,7 @@
 apply (rule nat_infinite)
 done
 
-interpretation FreeUltrafilterNat: freeultrafilter [FreeUltrafilterNat]
+interpretation FreeUltrafilterNat!: freeultrafilter FreeUltrafilterNat
 by (rule freeultrafilter_FreeUltrafilterNat)
 
 text {* This rule takes the place of the old ultra tactic *}
diff -r 918687637307 -r 3adc06d6504f src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/ROOT.ML	Thu Dec 18 20:19:49 2008 +0100
@@ -3,6 +3,7 @@
 Classical Higher-order Logic -- batteries included.
 *)
 
+set new_locales;
 use_thy "Complex_Main";
 
 val HOL_proofs = ! Proofterm.proofs;
diff -r 918687637307 -r 3adc06d6504f src/HOL/Real/HahnBanach/Bounds.thy
--- a/src/HOL/Real/HahnBanach/Bounds.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Bounds.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Real/HahnBanach/Bounds.thy
-    ID:         $Id$
     Author:     Gertrud Bauer, TU Munich
 *)
 
@@ -27,7 +26,7 @@
   assumes "lub A x"
   shows "\<Squnion>A = (x::'a::order)"
 proof -
-  interpret lub [A x] by fact
+  interpret lub A x by fact
   show ?thesis
   proof (unfold the_lub_def)
     from `lub A x` show "The (lub A) = x"
diff -r 918687637307 -r 3adc06d6504f src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Real/HahnBanach/FunctionNorm.thy
-    ID:         $Id$
     Author:     Gertrud Bauer, TU Munich
 *)
 
@@ -22,7 +21,7 @@
   linear forms:
 *}
 
-locale continuous = var V + norm_syntax + linearform +
+locale continuous = var_V + norm_syntax + linearform +
   assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
 
 declare continuous.intro [intro?] continuous_axioms.intro [intro?]
@@ -91,7 +90,7 @@
   assumes "continuous V norm f"
   shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
 proof -
-  interpret continuous [V norm f] by fact
+  interpret continuous V norm f by fact
   txt {* The existence of the supremum is shown using the
     completeness of the reals. Completeness means, that every
     non-empty bounded set of reals has a supremum. *}
@@ -159,7 +158,7 @@
   assumes b: "b \<in> B V f"
   shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
 proof -
-  interpret continuous [V norm f] by fact
+  interpret continuous V norm f by fact
   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
     using `continuous V norm f` by (rule fn_norm_works)
   from this and b show ?thesis ..
@@ -170,7 +169,7 @@
   assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
   shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
 proof -
-  interpret continuous [V norm f] by fact
+  interpret continuous V norm f by fact
   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
     using `continuous V norm f` by (rule fn_norm_works)
   from this and b show ?thesis ..
@@ -182,7 +181,7 @@
   assumes "continuous V norm f"
   shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
 proof -
-  interpret continuous [V norm f] by fact
+  interpret continuous V norm f by fact
   txt {* The function norm is defined as the supremum of @{text B}.
     So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
     0"}, provided the supremum exists and @{text B} is not empty. *}
@@ -204,8 +203,8 @@
   assumes x: "x \<in> V"
   shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
 proof -
-  interpret continuous [V norm f] by fact
-  interpret linearform [V f] .
+  interpret continuous V norm f by fact
+  interpret linearform V f .
   show ?thesis
   proof cases
     assume "x = 0"
@@ -246,7 +245,7 @@
   assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
   shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
 proof -
-  interpret continuous [V norm f] by fact
+  interpret continuous V norm f by fact
   show ?thesis
   proof (rule fn_norm_leastB [folded B_def fn_norm_def])
     fix b assume b: "b \<in> B V f"
diff -r 918687637307 -r 3adc06d6504f src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Real/HahnBanach/HahnBanach.thy
-    ID:         $Id$
     Author:     Gertrud Bauer, TU Munich
 *)
 
@@ -63,10 +62,10 @@
     -- {* and @{text f} a linear form on @{text F} such that @{text f} is bounded by @{text p}, *}
     -- {* then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \skp *}
 proof -
-  interpret vectorspace [E] by fact
-  interpret subspace [F E] by fact
-  interpret seminorm [E p] by fact
-  interpret linearform [F f] by fact
+  interpret vectorspace E by fact
+  interpret subspace F E by fact
+  interpret seminorm E p by fact
+  interpret linearform F f by fact
   def M \<equiv> "norm_pres_extensions E p F f"
   then have M: "M = \<dots>" by (simp only:)
   from E have F: "vectorspace F" ..
@@ -322,10 +321,10 @@
     \<and> (\<forall>x \<in> F. g x = f x)
     \<and> (\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x)"
 proof -
-  interpret vectorspace [E] by fact
-  interpret subspace [F E] by fact
-  interpret linearform [F f] by fact
-  interpret seminorm [E p] by fact
+  interpret vectorspace E by fact
+  interpret subspace F E by fact
+  interpret linearform F f by fact
+  interpret seminorm E p by fact
   have "\<exists>g. linearform E g \<and> (\<forall>x \<in> F. g x = f x) \<and> (\<forall>x \<in> E. g x \<le> p x)"
     using E FE sn lf
   proof (rule HahnBanach)
@@ -363,12 +362,12 @@
      \<and> (\<forall>x \<in> F. g x = f x)
      \<and> \<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
 proof -
-  interpret normed_vectorspace [E norm] by fact
-  interpret normed_vectorspace_with_fn_norm [E norm B fn_norm]
+  interpret normed_vectorspace E norm by fact
+  interpret normed_vectorspace_with_fn_norm E norm B fn_norm
     by (auto simp: B_def fn_norm_def) intro_locales
-  interpret subspace [F E] by fact
-  interpret linearform [F f] by fact
-  interpret continuous [F norm f] by fact
+  interpret subspace F E by fact
+  interpret linearform F f by fact
+  interpret continuous F norm f by fact
   have E: "vectorspace E" by intro_locales
   have F: "vectorspace F" by rule intro_locales
   have F_norm: "normed_vectorspace F norm"
diff -r 918687637307 -r 3adc06d6504f src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
-    ID:         $Id$
     Author:     Gertrud Bauer, TU Munich
 *)
 
@@ -46,7 +45,7 @@
   assumes r: "\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v"
   shows "\<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"
 proof -
-  interpret vectorspace [F] by fact
+  interpret vectorspace F by fact
   txt {* From the completeness of the reals follows:
     The set @{text "S = {a u. u \<in> F}"} has a supremum, if it is
     non-empty and has an upper bound. *}
@@ -98,8 +97,8 @@
   assumes E: "vectorspace E"
   shows "linearform H' h'"
 proof -
-  interpret linearform [H h] by fact
-  interpret vectorspace [E] by fact
+  interpret linearform H h by fact
+  interpret vectorspace E by fact
   show ?thesis
   proof
     note E = `vectorspace E`
@@ -203,10 +202,10 @@
     and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y"
   shows "\<forall>x \<in> H'. h' x \<le> p x"
 proof -
-  interpret vectorspace [E] by fact
-  interpret subspace [H E] by fact
-  interpret seminorm [E p] by fact
-  interpret linearform [H h] by fact
+  interpret vectorspace E by fact
+  interpret subspace H E by fact
+  interpret seminorm E p by fact
+  interpret linearform H h by fact
   show ?thesis
   proof
     fix x assume x': "x \<in> H'"
diff -r 918687637307 -r 3adc06d6504f src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -405,10 +405,10 @@
     and "linearform H h"
   shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R")
 proof
-  interpret subspace [H E] by fact
-  interpret vectorspace [E] by fact
-  interpret seminorm [E p] by fact
-  interpret linearform [H h] by fact
+  interpret subspace H E by fact
+  interpret vectorspace E by fact
+  interpret seminorm E p by fact
+  interpret linearform H h by fact
   have H: "vectorspace H" using `vectorspace E` ..
   {
     assume l: ?L
diff -r 918687637307 -r 3adc06d6504f src/HOL/Real/HahnBanach/Linearform.thy
--- a/src/HOL/Real/HahnBanach/Linearform.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Linearform.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Real/HahnBanach/Linearform.thy
-    ID:         $Id$
     Author:     Gertrud Bauer, TU Munich
 *)
 
@@ -14,8 +13,8 @@
   that is additive and multiplicative.
 *}
 
-locale linearform = var V + var f +
-  constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
+locale linearform =
+  fixes V :: "'a\<Colon>{minus, plus, zero, uminus} set" and f
   assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
     and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"
 
@@ -25,7 +24,7 @@
   assumes "vectorspace V"
   shows "x \<in> V \<Longrightarrow> f (- x) = - f x"
 proof -
-  interpret vectorspace [V] by fact
+  interpret vectorspace V by fact
   assume x: "x \<in> V"
   then have "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
   also from x have "\<dots> = (- 1) * (f x)" by (rule mult)
@@ -37,7 +36,7 @@
   assumes "vectorspace V"
   shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y"
 proof -
-  interpret vectorspace [V] by fact
+  interpret vectorspace V by fact
   assume x: "x \<in> V" and y: "y \<in> V"
   then have "x - y = x + - y" by (rule diff_eq1)
   also have "f \<dots> = f x + f (- y)" by (rule add) (simp_all add: x y)
@@ -51,7 +50,7 @@
   assumes "vectorspace V"
   shows "f 0 = 0"
 proof -
-  interpret vectorspace [V] by fact
+  interpret vectorspace V by fact
   have "f 0 = f (0 - 0)" by simp
   also have "\<dots> = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all
   also have "\<dots> = 0" by simp
diff -r 918687637307 -r 3adc06d6504f src/HOL/Real/HahnBanach/NormedSpace.thy
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Real/HahnBanach/NormedSpace.thy
-    ID:         $Id$
     Author:     Gertrud Bauer, TU Munich
 *)
 
@@ -20,7 +19,7 @@
 locale norm_syntax =
   fixes norm :: "'a \<Rightarrow> real"    ("\<parallel>_\<parallel>")
 
-locale seminorm = var V + norm_syntax +
+locale seminorm = var_V + norm_syntax +
   constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
   assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
     and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
@@ -32,7 +31,7 @@
   assumes "vectorspace V"
   shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
 proof -
-  interpret vectorspace [V] by fact
+  interpret vectorspace V by fact
   assume x: "x \<in> V" and y: "y \<in> V"
   then have "x - y = x + - 1 \<cdot> y"
     by (simp add: diff_eq2 negate_eq2a)
@@ -48,7 +47,7 @@
   assumes "vectorspace V"
   shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
 proof -
-  interpret vectorspace [V] by fact
+  interpret vectorspace V by fact
   assume x: "x \<in> V"
   then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
   also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>"
@@ -103,8 +102,8 @@
   assumes "subspace F E" "normed_vectorspace E norm"
   shows "normed_vectorspace F norm"
 proof -
-  interpret subspace [F E] by fact
-  interpret normed_vectorspace [E norm] by fact
+  interpret subspace F E by fact
+  interpret normed_vectorspace E norm by fact
   show ?thesis
   proof
     show "vectorspace F" by (rule vectorspace) unfold_locales
diff -r 918687637307 -r 3adc06d6504f src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Real/HahnBanach/Subspace.thy
-    ID:         $Id$
     Author:     Gertrud Bauer, TU Munich
 *)
 
@@ -17,8 +16,8 @@
   and scalar multiplication.
 *}
 
-locale subspace = var U + var V +
-  constrains U :: "'a\<Colon>{minus, plus, zero, uminus} set"
+locale subspace =
+  fixes U :: "'a\<Colon>{minus, plus, zero, uminus} set" and V
   assumes non_empty [iff, intro]: "U \<noteq> {}"
     and subset [iff]: "U \<subseteq> V"
     and add_closed [iff]: "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
@@ -46,7 +45,7 @@
   assumes x: "x \<in> U" and y: "y \<in> U"
   shows "x - y \<in> U"
 proof -
-  interpret vectorspace [V] by fact
+  interpret vectorspace V by fact
   from x y show ?thesis by (simp add: diff_eq1 negate_eq1)
 qed
 
@@ -60,11 +59,11 @@
   assumes "vectorspace V"
   shows "0 \<in> U"
 proof -
-  interpret vectorspace [V] by fact
-  have "U \<noteq> {}" by (rule U_V.non_empty)
+  interpret V!: vectorspace V by fact
+  have "U \<noteq> {}" by (rule non_empty)
   then obtain x where x: "x \<in> U" by blast
   then have "x \<in> V" .. then have "0 = x - x" by simp
-  also from `vectorspace V` x x have "\<dots> \<in> U" by (rule U_V.diff_closed)
+  also from `vectorspace V` x x have "\<dots> \<in> U" by (rule diff_closed)
   finally show ?thesis .
 qed
 
@@ -73,7 +72,7 @@
   assumes x: "x \<in> U"
   shows "- x \<in> U"
 proof -
-  interpret vectorspace [V] by fact
+  interpret vectorspace V by fact
   from x show ?thesis by (simp add: negate_eq1)
 qed
 
@@ -83,7 +82,7 @@
   assumes "vectorspace V"
   shows "vectorspace U"
 proof -
-  interpret vectorspace [V] by fact
+  interpret vectorspace V by fact
   show ?thesis
   proof
     show "U \<noteq> {}" ..
@@ -255,8 +254,8 @@
   assumes "vectorspace U" "vectorspace V"
   shows "U \<unlhd> U + V"
 proof -
-  interpret vectorspace [U] by fact
-  interpret vectorspace [V] by fact
+  interpret vectorspace U by fact
+  interpret vectorspace V by fact
   show ?thesis
   proof
     show "U \<noteq> {}" ..
@@ -279,9 +278,9 @@
   assumes "subspace U E" "vectorspace E" "subspace V E"
   shows "U + V \<unlhd> E"
 proof -
-  interpret subspace [U E] by fact
-  interpret vectorspace [E] by fact
-  interpret subspace [V E] by fact
+  interpret subspace U E by fact
+  interpret vectorspace E by fact
+  interpret subspace V E by fact
   show ?thesis
   proof
     have "0 \<in> U + V"
@@ -346,9 +345,9 @@
     and sum: "u1 + v1 = u2 + v2"
   shows "u1 = u2 \<and> v1 = v2"
 proof -
-  interpret vectorspace [E] by fact
-  interpret subspace [U E] by fact
-  interpret subspace [V E] by fact
+  interpret vectorspace E by fact
+  interpret subspace U E by fact
+  interpret subspace V E by fact
   show ?thesis
   proof
     have U: "vectorspace U"  (* FIXME: use interpret *)
@@ -395,8 +394,8 @@
     and eq: "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'"
   shows "y1 = y2 \<and> a1 = a2"
 proof -
-  interpret vectorspace [E] by fact
-  interpret subspace [H E] by fact
+  interpret vectorspace E by fact
+  interpret subspace H E by fact
   show ?thesis
   proof
     have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'"
@@ -451,8 +450,8 @@
     and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
   shows "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
 proof -
-  interpret vectorspace [E] by fact
-  interpret subspace [H E] by fact
+  interpret vectorspace E by fact
+  interpret subspace H E by fact
   show ?thesis
   proof (rule, simp_all only: split_paired_all split_conv)
     from t x' show "t = t + 0 \<cdot> x' \<and> t \<in> H" by simp
@@ -483,8 +482,8 @@
     and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
   shows "h' x = h y + a * xi"
 proof -
-  interpret vectorspace [E] by fact
-  interpret subspace [H E] by fact
+  interpret vectorspace E by fact
+  interpret subspace H E by fact
   from x y x' have "x \<in> H + lin x'" by auto
   have "\<exists>!p. (\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) p" (is "\<exists>!p. ?P p")
   proof (rule ex_ex1I)
diff -r 918687637307 -r 3adc06d6504f src/HOL/Real/HahnBanach/VectorSpace.thy
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -39,7 +39,9 @@
   the neutral element of scalar multiplication.
 *}
 
-locale vectorspace = var V +
+locale var_V = fixes V
+
+locale vectorspace = var_V +
   assumes non_empty [iff, intro?]: "V \<noteq> {}"
     and add_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y \<in> V"
     and mult_closed [iff]: "x \<in> V \<Longrightarrow> a \<cdot> x \<in> V"
diff -r 918687637307 -r 3adc06d6504f src/HOL/Real/HahnBanach/ZornLemma.thy
--- a/src/HOL/Real/HahnBanach/ZornLemma.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Real/HahnBanach/ZornLemma.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Real/HahnBanach/ZornLemma.thy
-    ID:         $Id$
     Author:     Gertrud Bauer, TU Munich
 *)
 
diff -r 918687637307 -r 3adc06d6504f src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Real/RealVector.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -60,7 +60,7 @@
   and scale_minus_left [simp]: "scale (- a) x = - (scale a x)"
   and scale_left_diff_distrib: "scale (a - b) x = scale a x - scale b x"
 proof -
-  interpret s: additive ["\<lambda>a. scale a x"]
+  interpret s: additive "\<lambda>a. scale a x"
     proof qed (rule scale_left_distrib)
   show "scale 0 x = 0" by (rule s.zero)
   show "scale (- a) x = - (scale a x)" by (rule s.minus)
@@ -71,7 +71,7 @@
   and scale_minus_right [simp]: "scale a (- x) = - (scale a x)"
   and scale_right_diff_distrib: "scale a (x - y) = scale a x - scale a y"
 proof -
-  interpret s: additive ["\<lambda>x. scale a x"]
+  interpret s: additive "\<lambda>x. scale a x"
     proof qed (rule scale_right_distrib)
   show "scale a 0 = 0" by (rule s.zero)
   show "scale a (- x) = - (scale a x)" by (rule s.minus)
@@ -151,8 +151,8 @@
   and scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x"
   and scaleR_one [simp]: "scaleR 1 x = x"
 
-interpretation real_vector:
-  vector_space ["scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"]
+interpretation real_vector!:
+  vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
 apply unfold_locales
 apply (rule scaleR_right_distrib)
 apply (rule scaleR_left_distrib)
@@ -195,10 +195,10 @@
 apply (rule mult_left_commute)
 done
 
-interpretation scaleR_left: additive ["(\<lambda>a. scaleR a x::'a::real_vector)"]
+interpretation scaleR_left!: additive "(\<lambda>a. scaleR a x::'a::real_vector)"
 proof qed (rule scaleR_left_distrib)
 
-interpretation scaleR_right: additive ["(\<lambda>x. scaleR a x::'a::real_vector)"]
+interpretation scaleR_right!: additive "(\<lambda>x. scaleR a x::'a::real_vector)"
 proof qed (rule scaleR_right_distrib)
 
 lemma nonzero_inverse_scaleR_distrib:
@@ -796,8 +796,8 @@
 
 end
 
-interpretation mult:
-  bounded_bilinear ["op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"]
+interpretation mult!:
+  bounded_bilinear "op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"
 apply (rule bounded_bilinear.intro)
 apply (rule left_distrib)
 apply (rule right_distrib)
@@ -807,19 +807,19 @@
 apply (simp add: norm_mult_ineq)
 done
 
-interpretation mult_left:
-  bounded_linear ["(\<lambda>x::'a::real_normed_algebra. x * y)"]
+interpretation mult_left!:
+  bounded_linear "(\<lambda>x::'a::real_normed_algebra. x * y)"
 by (rule mult.bounded_linear_left)
 
-interpretation mult_right:
-  bounded_linear ["(\<lambda>y::'a::real_normed_algebra. x * y)"]
+interpretation mult_right!:
+  bounded_linear "(\<lambda>y::'a::real_normed_algebra. x * y)"
 by (rule mult.bounded_linear_right)
 
-interpretation divide:
-  bounded_linear ["(\<lambda>x::'a::real_normed_field. x / y)"]
+interpretation divide!:
+  bounded_linear "(\<lambda>x::'a::real_normed_field. x / y)"
 unfolding divide_inverse by (rule mult.bounded_linear_left)
 
-interpretation scaleR: bounded_bilinear ["scaleR"]
+interpretation scaleR!: bounded_bilinear "scaleR"
 apply (rule bounded_bilinear.intro)
 apply (rule scaleR_left_distrib)
 apply (rule scaleR_right_distrib)
@@ -829,13 +829,13 @@
 apply (simp add: norm_scaleR)
 done
 
-interpretation scaleR_left: bounded_linear ["\<lambda>r. scaleR r x"]
+interpretation scaleR_left!: bounded_linear "\<lambda>r. scaleR r x"
 by (rule scaleR.bounded_linear_left)
 
-interpretation scaleR_right: bounded_linear ["\<lambda>x. scaleR r x"]
+interpretation scaleR_right!: bounded_linear "\<lambda>x. scaleR r x"
 by (rule scaleR.bounded_linear_right)
 
-interpretation of_real: bounded_linear ["\<lambda>r. of_real r"]
+interpretation of_real!: bounded_linear "\<lambda>r. of_real r"
 unfolding of_real_def by (rule scaleR.bounded_linear_left)
 
 end
diff -r 918687637307 -r 3adc06d6504f src/HOL/Statespace/StateSpaceEx.thy
--- a/src/HOL/Statespace/StateSpaceEx.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Statespace/StateSpaceEx.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -37,7 +37,7 @@
 projection~/ injection functions that convert from abstract values to
 @{typ "nat"} and @{text "bool"}. The logical content of the locale is: *}
 
-locale vars' =
+class_locale vars' =
   fixes n::'name and b::'name
   assumes "distinct [n, b]" 
 
@@ -204,7 +204,7 @@
   assumes "foo f a b c p1 i1 p2 i2 p3 i3 p4 i4"
   shows True
 proof
-  interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact
+  class_interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact
   term "s<a := i>\<cdot>a = i"
 qed
 
diff -r 918687637307 -r 3adc06d6504f src/HOL/Statespace/StateSpaceLocale.thy
--- a/src/HOL/Statespace/StateSpaceLocale.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Statespace/StateSpaceLocale.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -16,7 +16,7 @@
 concrete values.*}
 
 
-locale project_inject =
+class_locale project_inject =
  fixes project :: "'value \<Rightarrow> 'a"
  and   "inject":: "'a \<Rightarrow> 'value"
  assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"
diff -r 918687637307 -r 3adc06d6504f src/HOL/Word/TdThs.thy
--- a/src/HOL/Word/TdThs.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Word/TdThs.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -90,7 +90,7 @@
 
 end
 
-interpretation nat_int: type_definition [int nat "Collect (op <= 0)"]
+interpretation nat_int!: type_definition int nat "Collect (op <= 0)"
   by (rule td_nat_int)
 
 declare
diff -r 918687637307 -r 3adc06d6504f src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Word/WordArith.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -22,7 +22,7 @@
 proof
 qed (unfold word_sle_def word_sless_def, auto)
 
-interpretation signed: linorder ["word_sle" "word_sless"] 
+class_interpretation signed: linorder ["word_sle" "word_sless"] 
   by (rule signed_linorder)
 
 lemmas word_arith_wis = 
@@ -858,11 +858,11 @@
 lemmas td_ext_unat = refl [THEN td_ext_unat']
 lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm, standard]
 
-interpretation word_unat:
-  td_ext ["unat::'a::len word => nat" 
-          of_nat 
-          "unats (len_of TYPE('a::len))"
-          "%i. i mod 2 ^ len_of TYPE('a::len)"]
+interpretation word_unat!:
+  td_ext "unat::'a::len word => nat" 
+         of_nat 
+         "unats (len_of TYPE('a::len))"
+         "%i. i mod 2 ^ len_of TYPE('a::len)"
   by (rule td_ext_unat)
 
 lemmas td_unat = word_unat.td_thm
diff -r 918687637307 -r 3adc06d6504f src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Word/WordBitwise.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -344,11 +344,11 @@
 
 lemmas td_ext_nth = td_ext_nth' [OF refl refl refl, unfolded word_size]
 
-interpretation test_bit:
-  td_ext ["op !! :: 'a::len0 word => nat => bool"
-          set_bits
-          "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
-          "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"]
+interpretation test_bit!:
+  td_ext "op !! :: 'a::len0 word => nat => bool"
+         set_bits
+         "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
+         "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"
   by (rule td_ext_nth)
 
 declare test_bit.Rep' [simp del]
diff -r 918687637307 -r 3adc06d6504f src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Word/WordDefinition.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -356,11 +356,11 @@
 
 lemmas int_word_uint = td_ext_uint [THEN td_ext.eq_norm, standard]
 
-interpretation word_uint: 
-  td_ext ["uint::'a::len0 word \<Rightarrow> int" 
-          word_of_int 
-          "uints (len_of TYPE('a::len0))"
-          "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"]
+interpretation word_uint!:
+  td_ext "uint::'a::len0 word \<Rightarrow> int" 
+         word_of_int 
+         "uints (len_of TYPE('a::len0))"
+         "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"
   by (rule td_ext_uint)
   
 lemmas td_uint = word_uint.td_thm
@@ -368,11 +368,11 @@
 lemmas td_ext_ubin = td_ext_uint 
   [simplified len_gt_0 no_bintr_alt1 [symmetric]]
 
-interpretation word_ubin:
-  td_ext ["uint::'a::len0 word \<Rightarrow> int" 
-          word_of_int 
-          "uints (len_of TYPE('a::len0))"
-          "bintrunc (len_of TYPE('a::len0))"]
+interpretation word_ubin!:
+  td_ext "uint::'a::len0 word \<Rightarrow> int" 
+         word_of_int 
+         "uints (len_of TYPE('a::len0))"
+         "bintrunc (len_of TYPE('a::len0))"
   by (rule td_ext_ubin)
 
 lemma sint_sbintrunc': 
@@ -423,19 +423,19 @@
    and interpretations do not produce thm duplicates. I.e. 
    we get the name word_sint.Rep_eqD, but not word_sbin.Req_eqD,
    because the latter is the same thm as the former *)
-interpretation word_sint:
-  td_ext ["sint ::'a::len word => int" 
+interpretation word_sint!:
+  td_ext "sint ::'a::len word => int" 
           word_of_int 
           "sints (len_of TYPE('a::len))"
           "%w. (w + 2^(len_of TYPE('a::len) - 1)) mod 2^len_of TYPE('a::len) -
-               2 ^ (len_of TYPE('a::len) - 1)"]
+               2 ^ (len_of TYPE('a::len) - 1)"
   by (rule td_ext_sint)
 
-interpretation word_sbin:
-  td_ext ["sint ::'a::len word => int" 
+interpretation word_sbin!:
+  td_ext "sint ::'a::len word => int" 
           word_of_int 
           "sints (len_of TYPE('a::len))"
-          "sbintrunc (len_of TYPE('a::len) - 1)"]
+          "sbintrunc (len_of TYPE('a::len) - 1)"
   by (rule td_ext_sbin)
 
 lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm, standard]
@@ -635,10 +635,10 @@
   apply simp
   done
 
-interpretation word_bl:
-  type_definition ["to_bl :: 'a::len0 word => bool list"
-                   of_bl  
-                   "{bl. length bl = len_of TYPE('a::len0)}"]
+interpretation word_bl!:
+  type_definition "to_bl :: 'a::len0 word => bool list"
+                  of_bl  
+                  "{bl. length bl = len_of TYPE('a::len0)}"
   by (rule td_bl)
 
 lemma word_size_bl: "size w == size (to_bl w)"
diff -r 918687637307 -r 3adc06d6504f src/HOL/Word/WordGenLib.thy
--- a/src/HOL/Word/WordGenLib.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/Word/WordGenLib.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -107,16 +107,16 @@
   apply (rule word_or_not)
   done
 
-interpretation word_bool_alg:
-  boolean ["op AND" "op OR" bitNOT 0 max_word]
+interpretation word_bool_alg!:
+  boolean "op AND" "op OR" bitNOT 0 max_word
   by (rule word_boolean)
 
 lemma word_xor_and_or:
   "x XOR y = x AND NOT y OR NOT x AND (y::'a::len0 word)"
   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
 
-interpretation word_bool_alg:
-  boolean_xor ["op AND" "op OR" bitNOT 0 max_word "op XOR"]
+interpretation word_bool_alg!:
+  boolean_xor "op AND" "op OR" bitNOT 0 max_word "op XOR"
   apply (rule boolean_xor.intro)
    apply (rule word_boolean)
   apply (rule boolean_xor_axioms.intro)
@@ -363,7 +363,7 @@
    apply (erule contrapos_pn, simp)
    apply (drule arg_cong[where f=of_nat])
    apply simp
-   apply (subst (asm) word_unat.Rep_Abs_A.Rep_inverse[of n])
+   apply (subst (asm) word_unat.Rep_inverse[of n])
    apply simp
   apply simp
   done
diff -r 918687637307 -r 3adc06d6504f src/HOL/ex/Abstract_NAT.thy
--- a/src/HOL/ex/Abstract_NAT.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/ex/Abstract_NAT.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*
-    ID:         $Id$
     Author:     Makarius
 *)
 
@@ -131,7 +130,7 @@
 
 text {* \medskip Just see that our abstract specification makes sense \dots *}
 
-interpretation NAT [0 Suc]
+interpretation NAT 0 Suc
 proof (rule NAT.intro)
   fix m n
   show "(Suc m = Suc n) = (m = n)" by simp
diff -r 918687637307 -r 3adc06d6504f src/HOL/ex/LocaleTest2.thy
--- a/src/HOL/ex/LocaleTest2.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/ex/LocaleTest2.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/ex/LocaleTest2.thy
-    ID:         $Id$
     Author:     Clemens Ballarin
     Copyright (c) 2007 by Clemens Ballarin
 
@@ -433,8 +432,7 @@
 end
 
 
-interpretation dlo < dlat
-(* TODO: definition syntax is unavailable *)
+sublocale dlo < dlat
 proof
   fix x y
   from total have "is_inf x y (if x \<sqsubseteq> y then x else y)" by (auto simp: is_inf_def)
@@ -445,7 +443,7 @@
   then show "EX sup. is_sup x y sup" by blast
 qed
 
-interpretation dlo < ddlat
+sublocale dlo < ddlat
 proof
   fix x y z
   show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r")
@@ -470,13 +468,13 @@
 
 subsubsection {* Total order @{text "<="} on @{typ int} *}
 
-interpretation int: dpo ["op <= :: [int, int] => bool"]
+interpretation int!: dpo "op <= :: [int, int] => bool"
   where "(dpo.less (op <=) (x::int) y) = (x < y)"
   txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
 proof -
   show "dpo (op <= :: [int, int] => bool)"
     proof qed auto
-  then interpret int: dpo ["op <= :: [int, int] => bool"] .
+  then interpret int: dpo "op <= :: [int, int] => bool" .
     txt {* Gives interpreted version of @{text less_def} (without condition). *}
   show "(dpo.less (op <=) (x::int) y) = (x < y)"
     by (unfold int.less_def) auto
@@ -489,7 +487,7 @@
 lemma "(op < :: [int, int] => bool) = op <"
   apply (rule int.abs_test) done
 
-interpretation int: dlat ["op <= :: [int, int] => bool"]
+interpretation int!: dlat "op <= :: [int, int] => bool"
   where meet_eq: "dlat.meet (op <=) (x::int) y = min x y"
     and join_eq: "dlat.join (op <=) (x::int) y = max x y"
 proof -
@@ -498,7 +496,7 @@
     apply (unfold int.is_inf_def int.is_sup_def)
     apply arith+
     done
-  then interpret int: dlat ["op <= :: [int, int] => bool"] .
+  then interpret int: dlat "op <= :: [int, int] => bool" .
   txt {* Interpretation to ease use of definitions, which are
     conditional in general but unconditional after interpretation. *}
   show "dlat.meet (op <=) (x::int) y = min x y"
@@ -513,7 +511,7 @@
     by auto
 qed
 
-interpretation int: dlo ["op <= :: [int, int] => bool"]
+interpretation int!: dlo "op <= :: [int, int] => bool"
   proof qed arith
 
 text {* Interpreted theorems from the locales, involving defined terms. *}
@@ -526,13 +524,13 @@
 
 subsubsection {* Total order @{text "<="} on @{typ nat} *}
 
-interpretation nat: dpo ["op <= :: [nat, nat] => bool"]
+interpretation nat!: dpo "op <= :: [nat, nat] => bool"
   where "dpo.less (op <=) (x::nat) y = (x < y)"
   txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
 proof -
   show "dpo (op <= :: [nat, nat] => bool)"
     proof qed auto
-  then interpret nat: dpo ["op <= :: [nat, nat] => bool"] .
+  then interpret nat: dpo "op <= :: [nat, nat] => bool" .
     txt {* Gives interpreted version of @{text less_def} (without condition). *}
   show "dpo.less (op <=) (x::nat) y = (x < y)"
     apply (unfold nat.less_def)
@@ -540,7 +538,7 @@
     done
 qed
 
-interpretation nat: dlat ["op <= :: [nat, nat] => bool"]
+interpretation nat!: dlat "op <= :: [nat, nat] => bool"
   where "dlat.meet (op <=) (x::nat) y = min x y"
     and "dlat.join (op <=) (x::nat) y = max x y"
 proof -
@@ -549,7 +547,7 @@
     apply (unfold nat.is_inf_def nat.is_sup_def)
     apply arith+
     done
-  then interpret nat: dlat ["op <= :: [nat, nat] => bool"] .
+  then interpret nat: dlat "op <= :: [nat, nat] => bool" .
   txt {* Interpretation to ease use of definitions, which are
     conditional in general but unconditional after interpretation. *}
   show "dlat.meet (op <=) (x::nat) y = min x y"
@@ -564,7 +562,7 @@
     by auto
 qed
 
-interpretation nat: dlo ["op <= :: [nat, nat] => bool"]
+interpretation nat!: dlo "op <= :: [nat, nat] => bool"
   proof qed arith
 
 text {* Interpreted theorems from the locales, involving defined terms. *}
@@ -577,13 +575,13 @@
 
 subsubsection {* Lattice @{text "dvd"} on @{typ nat} *}
 
-interpretation nat_dvd: dpo ["op dvd :: [nat, nat] => bool"]
+interpretation nat_dvd!: dpo "op dvd :: [nat, nat] => bool"
   where "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
   txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
 proof -
   show "dpo (op dvd :: [nat, nat] => bool)"
     proof qed (auto simp: dvd_def)
-  then interpret nat_dvd: dpo ["op dvd :: [nat, nat] => bool"] .
+  then interpret nat_dvd: dpo "op dvd :: [nat, nat] => bool" .
     txt {* Gives interpreted version of @{text less_def} (without condition). *}
   show "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
     apply (unfold nat_dvd.less_def)
@@ -591,7 +589,7 @@
     done
 qed
 
-interpretation nat_dvd: dlat ["op dvd :: [nat, nat] => bool"]
+interpretation nat_dvd!: dlat "op dvd :: [nat, nat] => bool"
   where "dlat.meet (op dvd) (x::nat) y = gcd x y"
     and "dlat.join (op dvd) (x::nat) y = lcm x y"
 proof -
@@ -603,7 +601,7 @@
     apply (rule_tac x = "lcm x y" in exI)
     apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
     done
-  then interpret nat_dvd: dlat ["op dvd :: [nat, nat] => bool"] .
+  then interpret nat_dvd: dlat "op dvd :: [nat, nat] => bool" .
   txt {* Interpretation to ease use of definitions, which are
     conditional in general but unconditional after interpretation. *}
   show "dlat.meet (op dvd) (x::nat) y = gcd x y"
@@ -819,7 +817,8 @@
 end
 
 
-locale Dhom = Dgrp prod (infixl "**" 65) one + Dgrp sum (infixl "+++" 60) zero +
+locale Dhom = prod: Dgrp prod one + sum: Dgrp sum zero
+    for prod (infixl "**" 65) and one and sum (infixl "+++" 60) and zero +
   fixes hom
   assumes hom_mult [simp]: "hom (x ** y) = hom x +++ hom y"
 
@@ -838,14 +837,14 @@
 
 subsubsection {* Interpretation of Functions *}
 
-interpretation Dfun: Dmonoid ["op o" "id :: 'a => 'a"]
+interpretation Dfun!: Dmonoid "op o" "id :: 'a => 'a"
   where "Dmonoid.unit (op o) id f = bij (f::'a => 'a)"
 (*    and "Dmonoid.inv (op o) id" = "inv :: ('a => 'a) => ('a => 'a)" *)
 proof -
   show "Dmonoid op o (id :: 'a => 'a)" proof qed (simp_all add: o_assoc)
   note Dmonoid = this
 (*
-  from this interpret Dmonoid ["op o" "id :: 'a => 'a"] .
+  from this interpret Dmonoid "op o" "id :: 'a => 'a" .
 *)
   show "Dmonoid.unit (op o) (id :: 'a => 'a) f = bij f"
     apply (unfold Dmonoid.unit_def [OF Dmonoid])
@@ -888,7 +887,7 @@
   "(f :: unit => unit) = id"
   by rule simp
 
-interpretation Dfun: Dgrp ["op o" "id :: unit => unit"]
+interpretation Dfun!: Dgrp "op o" "id :: unit => unit"
   where "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
 proof -
   have "Dmonoid op o (id :: 'a => 'a)" ..
diff -r 918687637307 -r 3adc06d6504f src/HOL/ex/Tarski.thy
--- a/src/HOL/ex/Tarski.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/ex/Tarski.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -120,7 +120,7 @@
 locale CL = S +
   assumes cl_co:  "cl : CompleteLattice"
 
-interpretation CL < PO
+sublocale CL < PO
 apply (simp_all add: A_def r_def)
 apply unfold_locales
 using cl_co unfolding CompleteLattice_def by auto
@@ -131,7 +131,7 @@
   assumes f_cl:  "(cl,f) : CLF_set" (*was the equivalent "f : CLF_set``{cl}"*)
   defines P_def: "P == fix f A"
 
-interpretation CLF < CL
+sublocale CLF < CL
 apply (simp_all add: A_def r_def)
 apply unfold_locales
 using f_cl unfolding CLF_set_def by auto
diff -r 918687637307 -r 3adc06d6504f src/HOL/main.ML
--- a/src/HOL/main.ML	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/main.ML	Thu Dec 18 20:19:49 2008 +0100
@@ -4,4 +4,5 @@
 Classical Higher-order Logic -- only "Main".
 *)
 
+set new_locales;
 use_thy "Main";
diff -r 918687637307 -r 3adc06d6504f src/HOL/plain.ML
--- a/src/HOL/plain.ML	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOL/plain.ML	Thu Dec 18 20:19:49 2008 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/plain.ML
-    ID:         $Id$
  
 Classical Higher-order Logic -- plain Tool bootstrap.
 *)
 
+set new_locales;
 use_thy "Plain";
diff -r 918687637307 -r 3adc06d6504f src/HOLCF/Algebraic.thy
--- a/src/HOLCF/Algebraic.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOLCF/Algebraic.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Algebraic.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
@@ -161,7 +160,7 @@
   assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
   shows "pre_deflation (d oo f)"
 proof
-  interpret d: finite_deflation [d] by fact
+  interpret d: finite_deflation d by fact
   fix x
   show "\<And>x. (d oo f)\<cdot>x \<sqsubseteq> x"
     by (simp, rule trans_less [OF d.less f])
@@ -174,9 +173,9 @@
   assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
   shows "eventual (\<lambda>n. iterate n\<cdot>(d oo f))\<cdot>x = x \<longleftrightarrow> d\<cdot>x = x \<and> f\<cdot>x = x"
 proof -
-  interpret d: finite_deflation [d] by fact
+  interpret d: finite_deflation d by fact
   let ?e = "d oo f"
-  interpret e: pre_deflation ["d oo f"]
+  interpret e: pre_deflation "d oo f"
     using `finite_deflation d` f
     by (rule pre_deflation_d_f)
   let ?g = "eventual (\<lambda>n. iterate n\<cdot>?e)"
@@ -216,7 +215,7 @@
 lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
 using Rep_fin_defl by simp
 
-interpretation Rep_fin_defl: finite_deflation ["Rep_fin_defl d"]
+interpretation Rep_fin_defl!: finite_deflation "Rep_fin_defl d"
 by (rule finite_deflation_Rep_fin_defl)
 
 lemma fin_defl_lessI:
@@ -321,7 +320,7 @@
 apply (rule Rep_fin_defl.compact)
 done
 
-interpretation fin_defl: basis_take [sq_le fd_take]
+interpretation fin_defl!: basis_take sq_le fd_take
 apply default
 apply (rule fd_take_less)
 apply (rule fd_take_idem)
@@ -371,8 +370,8 @@
 unfolding alg_defl_principal_def
 by (simp add: Abs_alg_defl_inverse sq_le.ideal_principal)
 
-interpretation alg_defl:
-  ideal_completion [sq_le fd_take alg_defl_principal Rep_alg_defl]
+interpretation alg_defl!:
+  ideal_completion sq_le fd_take alg_defl_principal Rep_alg_defl
 apply default
 apply (rule ideal_Rep_alg_defl)
 apply (erule Rep_alg_defl_lub)
@@ -462,7 +461,7 @@
 apply (rule finite_deflation_Rep_fin_defl)
 done
 
-interpretation cast: deflation ["cast\<cdot>d"]
+interpretation cast!: deflation "cast\<cdot>d"
 by (rule deflation_cast)
 
 lemma "cast\<cdot>(\<Squnion>i. alg_defl_principal (Abs_fin_defl (approx i)))\<cdot>x = x"
@@ -486,7 +485,7 @@
   constrains e :: "'a::profinite \<rightarrow> 'b::profinite"
   shows "\<exists>d. cast\<cdot>d = e oo p"
 proof
-  interpret ep_pair [e p] by fact
+  interpret ep_pair e p by fact
   let ?a = "\<lambda>i. e oo approx i oo p"
   have a: "\<And>i. finite_deflation (?a i)"
     apply (rule finite_deflation_e_d_p)
@@ -517,7 +516,7 @@
     "\<And>i. finite_deflation (a i)"
     "(\<Squnion>i. a i) = ID"
 proof
-  interpret ep_pair [e p] by fact
+  interpret ep_pair e p by fact
   let ?a = "\<lambda>i. p oo cast\<cdot>(approx i\<cdot>d) oo e"
   show "\<And>i. finite_deflation (?a i)"
     apply (rule finite_deflation_p_d_e)
diff -r 918687637307 -r 3adc06d6504f src/HOLCF/Bifinite.thy
--- a/src/HOLCF/Bifinite.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOLCF/Bifinite.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Bifinite.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
@@ -38,7 +37,7 @@
     by (rule finite_fixes_approx)
 qed
 
-interpretation approx: finite_deflation ["approx i"]
+interpretation approx!: finite_deflation "approx i"
 by (rule finite_deflation_approx)
 
 lemma (in deflation) deflation: "deflation d" ..
diff -r 918687637307 -r 3adc06d6504f src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOLCF/CompactBasis.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/CompactBasis.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
@@ -47,8 +46,8 @@
 
 lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric]
 
-interpretation compact_basis:
-  basis_take [sq_le compact_take]
+interpretation compact_basis!:
+  basis_take sq_le compact_take
 proof
   fix n :: nat and a :: "'a compact_basis"
   show "compact_take n a \<sqsubseteq> a"
@@ -93,8 +92,8 @@
   approximants :: "'a \<Rightarrow> 'a compact_basis set" where
   "approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
 
-interpretation compact_basis:
-  ideal_completion [sq_le compact_take Rep_compact_basis approximants]
+interpretation compact_basis!:
+  ideal_completion sq_le compact_take Rep_compact_basis approximants
 proof
   fix w :: 'a
   show "preorder.ideal sq_le (approximants w)"
@@ -245,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
+  interpret ab_semigroup_idem_mult f by fact
   show ?thesis unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
 qed
 
diff -r 918687637307 -r 3adc06d6504f src/HOLCF/Completion.thy
--- a/src/HOLCF/Completion.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOLCF/Completion.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Completion.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
@@ -157,7 +156,7 @@
 
 end
 
-interpretation sq_le: preorder ["sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"]
+interpretation sq_le!: preorder "sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"
 apply unfold_locales
 apply (rule refl_less)
 apply (erule (1) trans_less)
diff -r 918687637307 -r 3adc06d6504f src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOLCF/ConvexPD.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/ConvexPD.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
@@ -21,7 +20,7 @@
 lemma convex_le_trans: "\<lbrakk>t \<le>\<natural> u; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> t \<le>\<natural> v"
 unfolding convex_le_def by (fast intro: upper_le_trans lower_le_trans)
 
-interpretation convex_le: preorder [convex_le]
+interpretation convex_le!: preorder convex_le
 by (rule preorder.intro, rule convex_le_refl, rule convex_le_trans)
 
 lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<natural> t"
@@ -179,8 +178,8 @@
 unfolding convex_principal_def
 by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal)
 
-interpretation convex_pd:
-  ideal_completion [convex_le pd_take convex_principal Rep_convex_pd]
+interpretation convex_pd!:
+  ideal_completion convex_le pd_take convex_principal Rep_convex_pd
 apply unfold_locales
 apply (rule pd_take_convex_le)
 apply (rule pd_take_idem)
@@ -297,7 +296,7 @@
 apply (simp add: PDPlus_absorb)
 done
 
-interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\<natural>"]
+interpretation aci_convex_plus!: ab_semigroup_idem_mult "op +\<natural>"
   by unfold_locales
     (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+
 
diff -r 918687637307 -r 3adc06d6504f src/HOLCF/Deflation.thy
--- a/src/HOLCF/Deflation.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOLCF/Deflation.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Deflation.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
@@ -82,10 +81,10 @@
   assumes "deflation g"
   shows "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>(g\<cdot>x) = f\<cdot>x"
 proof (rule antisym_less)
-  interpret g: deflation [g] by fact
+  interpret g: deflation g by fact
   from g.less show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
 next
-  interpret f: deflation [f] by fact
+  interpret f: deflation f by fact
   assume "f \<sqsubseteq> g" hence "f\<cdot>x \<sqsubseteq> g\<cdot>x" by (rule monofun_cfun_fun)
   hence "f\<cdot>(f\<cdot>x) \<sqsubseteq> f\<cdot>(g\<cdot>x)" by (rule monofun_cfun_arg)
   also have "f\<cdot>(f\<cdot>x) = f\<cdot>x" by (rule f.idem)
@@ -220,7 +219,7 @@
   assumes "deflation d"
   shows "deflation (e oo d oo p)"
 proof
-  interpret deflation [d] by fact
+  interpret deflation d by fact
   fix x :: 'b
   show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
     by (simp add: idem)
@@ -232,7 +231,7 @@
   assumes "finite_deflation d"
   shows "finite_deflation (e oo d oo p)"
 proof
-  interpret finite_deflation [d] by fact
+  interpret finite_deflation d by fact
   fix x :: 'b
   show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
     by (simp add: idem)
@@ -251,7 +250,7 @@
   assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
   shows "deflation (p oo d oo e)"
 proof -
-  interpret d: deflation [d] by fact
+  interpret d: deflation d by fact
   {
     fix x
     have "d\<cdot>(e\<cdot>x) \<sqsubseteq> e\<cdot>x"
@@ -288,7 +287,7 @@
   assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
   shows "finite_deflation (p oo d oo e)"
 proof -
-  interpret d: finite_deflation [d] by fact
+  interpret d: finite_deflation d by fact
   show ?thesis
   proof (intro_locales)
     have "deflation d" ..
@@ -317,8 +316,8 @@
   assumes "ep_pair e1 p" and "ep_pair e2 p"
   shows "e1 \<sqsubseteq> e2"
 proof (rule less_cfun_ext)
-  interpret e1: ep_pair [e1 p] by fact
-  interpret e2: ep_pair [e2 p] by fact
+  interpret e1: ep_pair e1 p by fact
+  interpret e2: ep_pair e2 p by fact
   fix x
   have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x"
     by (rule e1.e_p_less)
@@ -334,8 +333,8 @@
   assumes "ep_pair e p1" and "ep_pair e p2"
   shows "p1 \<sqsubseteq> p2"
 proof (rule less_cfun_ext)
-  interpret p1: ep_pair [e p1] by fact
-  interpret p2: ep_pair [e p2] by fact
+  interpret p1: ep_pair e p1 by fact
+  interpret p2: ep_pair e p2 by fact
   fix x
   have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x"
     by (rule p1.e_p_less)
@@ -358,8 +357,8 @@
   assumes "ep_pair e1 p1" and "ep_pair e2 p2"
   shows "ep_pair (e2 oo e1) (p1 oo p2)"
 proof
-  interpret ep1: ep_pair [e1 p1] by fact
-  interpret ep2: ep_pair [e2 p2] by fact
+  interpret ep1: ep_pair e1 p1 by fact
+  interpret ep2: ep_pair e2 p2 by fact
   fix x y
   show "(p1 oo p2)\<cdot>((e2 oo e1)\<cdot>x) = x"
     by simp
diff -r 918687637307 -r 3adc06d6504f src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOLCF/LowerPD.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/LowerPD.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
@@ -27,7 +26,7 @@
 apply (erule (1) trans_less)
 done
 
-interpretation lower_le: preorder [lower_le]
+interpretation lower_le!: preorder lower_le
 by (rule preorder.intro, rule lower_le_refl, rule lower_le_trans)
 
 lemma lower_le_minimal [simp]: "PDUnit compact_bot \<le>\<flat> t"
@@ -134,8 +133,8 @@
 unfolding lower_principal_def
 by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal)
 
-interpretation lower_pd:
-  ideal_completion [lower_le pd_take lower_principal Rep_lower_pd]
+interpretation lower_pd!:
+  ideal_completion lower_le pd_take lower_principal Rep_lower_pd
 apply unfold_locales
 apply (rule pd_take_lower_le)
 apply (rule pd_take_idem)
@@ -251,7 +250,7 @@
 apply (simp add: PDPlus_absorb)
 done
 
-interpretation aci_lower_plus: ab_semigroup_idem_mult ["op +\<flat>"]
+interpretation aci_lower_plus!: ab_semigroup_idem_mult "op +\<flat>"
   by unfold_locales
     (rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+
 
diff -r 918687637307 -r 3adc06d6504f src/HOLCF/Universal.thy
--- a/src/HOLCF/Universal.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOLCF/Universal.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Universal.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
@@ -227,13 +226,13 @@
 apply (simp add: ubasis_take_same)
 done
 
-interpretation udom: preorder [ubasis_le]
+interpretation udom!: preorder ubasis_le
 apply default
 apply (rule ubasis_le_refl)
 apply (erule (1) ubasis_le_trans)
 done
 
-interpretation udom: basis_take [ubasis_le ubasis_take]
+interpretation udom!: basis_take ubasis_le ubasis_take
 apply default
 apply (rule ubasis_take_less)
 apply (rule ubasis_take_idem)
@@ -282,8 +281,8 @@
 unfolding udom_principal_def
 by (simp add: Abs_udom_inverse udom.ideal_principal)
 
-interpretation udom:
-  ideal_completion [ubasis_le ubasis_take udom_principal Rep_udom]
+interpretation udom!:
+  ideal_completion ubasis_le ubasis_take udom_principal Rep_udom
 apply unfold_locales
 apply (rule ideal_Rep_udom)
 apply (erule Rep_udom_lub)
diff -r 918687637307 -r 3adc06d6504f src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/HOLCF/UpperPD.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/UpperPD.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
@@ -27,7 +26,7 @@
 apply (erule (1) trans_less)
 done
 
-interpretation upper_le: preorder [upper_le]
+interpretation upper_le!: preorder upper_le
 by (rule preorder.intro, rule upper_le_refl, rule upper_le_trans)
 
 lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<sharp> t"
@@ -132,8 +131,8 @@
 unfolding upper_principal_def
 by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal)
 
-interpretation upper_pd:
-  ideal_completion [upper_le pd_take upper_principal Rep_upper_pd]
+interpretation upper_pd!:
+  ideal_completion upper_le pd_take upper_principal Rep_upper_pd
 apply unfold_locales
 apply (rule pd_take_upper_le)
 apply (rule pd_take_idem)
@@ -249,7 +248,7 @@
 apply (simp add: PDPlus_absorb)
 done
 
-interpretation aci_upper_plus: ab_semigroup_idem_mult ["op +\<sharp>"]
+interpretation aci_upper_plus!: ab_semigroup_idem_mult "op +\<sharp>"
   by unfold_locales
     (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+
 
diff -r 918687637307 -r 3adc06d6504f src/Pure/Isar/expression.ML
diff -r 918687637307 -r 3adc06d6504f src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Dec 18 20:19:49 2008 +0100
@@ -53,8 +53,7 @@
   val print_configs: Toplevel.transition -> Toplevel.transition
   val print_theorems: Toplevel.transition -> Toplevel.transition
   val print_locales: Toplevel.transition -> Toplevel.transition
-  val print_locale: bool * (Locale.expr * Element.context list)
-    -> Toplevel.transition -> Toplevel.transition
+  val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition
   val print_registrations: bool -> string -> Toplevel.transition -> Toplevel.transition
   val print_attributes: Toplevel.transition -> Toplevel.transition
   val print_simpset: Toplevel.transition -> Toplevel.transition
@@ -355,11 +354,11 @@
 val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof;
 
 val print_locales = Toplevel.unknown_theory o
-  Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
+  Toplevel.keep (NewLocale.print_locales o Toplevel.theory_of);
 
-fun print_locale (show_facts, (imports, body)) = Toplevel.unknown_theory o
+fun print_locale (show_facts, name) = Toplevel.unknown_theory o
   Toplevel.keep (fn state =>
-    Locale.print_locale (Toplevel.theory_of state) show_facts imports body);
+    NewLocale.print_locale (Toplevel.theory_of state) show_facts name);
 
 fun print_registrations show_wits name = Toplevel.unknown_context o
   Toplevel.keep (Toplevel.node_case
diff -r 918687637307 -r 3adc06d6504f src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Dec 18 20:19:49 2008 +0100
@@ -385,18 +385,18 @@
 (* locales *)
 
 val locale_val =
-  SpecParse.locale_expr --
+  SpecParse.locale_expression --
     Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
-  Scan.repeat1 SpecParse.context_element >> pair Locale.empty;
+  Scan.repeat1 SpecParse.context_element >> pair ([], []);
 
 val _ =
   OuterSyntax.command "locale" "define named proof context" K.thy_decl
-    (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, []) -- P.opt_begin
+    (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
       >> (fn ((name, (expr, elems)), begin) =>
           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
-            (Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin)));
-
-val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Binding.empty;
+            (Expression.add_locale_cmd name name expr elems #>
+              (fn ((target, notes), ctxt) => TheoryTarget.begin target ctxt |>
+                fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes))));
 
 val _ =
   OuterSyntax.command "sublocale"
@@ -407,6 +407,40 @@
 
 val _ =
   OuterSyntax.command "interpretation"
+    "prove interpretation of locale expression in theory" K.thy_goal
+    (P.!!! SpecParse.locale_expression --
+      Scan.optional (P.$$$ "where" |-- P.and_list1 (SpecParse.opt_thm_name ":" -- P.prop)) []
+        >> (fn (expr, equations) => Toplevel.print o
+            Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations)));
+
+val _ =
+  OuterSyntax.command "interpret"
+    "prove interpretation of locale expression in proof context"
+    (K.tag_proof K.prf_goal)
+    (P.!!! SpecParse.locale_expression
+        >> (fn expr => Toplevel.print o
+            Toplevel.proof' (fn int => Expression.interpret_cmd expr int)));
+
+local
+
+val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Binding.empty;
+
+in
+
+val locale_val =
+  SpecParse.locale_expr --
+    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
+  Scan.repeat1 SpecParse.context_element >> pair Locale.empty;
+
+val _ =
+  OuterSyntax.command "class_locale" "define named proof context based on classes" K.thy_decl
+    (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, []) -- P.opt_begin
+      >> (fn ((name, (expr, elems)), begin) =>
+          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
+            (Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin)));
+
+val _ =
+  OuterSyntax.command "class_interpretation"
     "prove and register interpretation of locale expression in theory or locale" K.thy_goal
     (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr
       >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) ||
@@ -416,7 +450,7 @@
               (Locale.interpretation_cmd (Binding.base_name name) expr insts)));
 
 val _ =
-  OuterSyntax.command "interpret"
+  OuterSyntax.command "class_interpret"
     "prove and register interpretation of locale expression in proof context"
     (K.tag_proof K.prf_goal)
     (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
@@ -424,6 +458,8 @@
           Toplevel.proof'
             (fn int => Locale.interpret_cmd (Binding.base_name name) expr insts int)));
 
+end;
+
 
 (* classes *)
 
@@ -817,7 +853,7 @@
 
 val _ =
   OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
-    (opt_bang -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
+    (opt_bang -- P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
 
 val _ =
   OuterSyntax.improper_command "print_interps"
diff -r 918687637307 -r 3adc06d6504f src/Pure/Isar/subclass.ML
--- a/src/Pure/Isar/subclass.ML	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/Pure/Isar/subclass.ML	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/subclass.ML
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
 User interface for proving subclass relationship between type classes.
@@ -22,7 +21,7 @@
     val thy = ProofContext.theory_of lthy;
     val sup = prep_class thy raw_sup;
     val sub = case TheoryTarget.peek lthy
-     of {is_class = false, ...} => error "No class context"
+     of {is_class = false, ...} => error "Not a class context"
       | {target, ...} => target;
     val _ = if Sign.subsort thy ([sup], [sub])
       then error ("Class " ^ Syntax.string_of_sort lthy [sup]
diff -r 918687637307 -r 3adc06d6504f src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/Pure/Isar/theory_target.ML	Thu Dec 18 20:19:49 2008 +0100
@@ -8,7 +8,7 @@
 
 signature THEORY_TARGET =
 sig
-  val peek: local_theory -> {target: string, is_locale: bool,
+  val peek: local_theory -> {target: string, new_locale: bool, is_locale: bool,
     is_class: bool, instantiation: string list * (string * sort) list * sort,
     overloading: (string * (string * typ) * bool) list}
   val init: string option -> theory -> local_theory
@@ -24,25 +24,32 @@
 
 (* new locales *)
 
-fun locale_extern x = if !new_locales then NewLocale.extern x else Locale.extern x;
-fun locale_add_type_syntax x = if !new_locales then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
-fun locale_add_term_syntax x = if !new_locales then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
-fun locale_add_declaration x = if !new_locales then NewLocale.add_declaration x else Locale.add_declaration x;
-fun locale_add_thmss x = if !new_locales then NewLocale.add_thmss x else Locale.add_thmss x;
-fun locale_init x = if !new_locales then NewLocale.init x else Locale.init x;
-fun locale_intern x = if !new_locales then NewLocale.intern x else Locale.intern x;
+fun locale_extern new_locale x = 
+  if !new_locales andalso new_locale then NewLocale.extern x else Locale.extern x;
+fun locale_add_type_syntax new_locale x =
+  if !new_locales andalso new_locale then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
+fun locale_add_term_syntax new_locale x =
+  if !new_locales andalso new_locale then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
+fun locale_add_declaration new_locale x =
+  if !new_locales andalso new_locale then NewLocale.add_declaration x else Locale.add_declaration x;
+fun locale_add_thmss new_locale x =
+  if !new_locales andalso new_locale then NewLocale.add_thmss x else Locale.add_thmss x;
+fun locale_init new_locale x =
+  if !new_locales andalso new_locale then NewLocale.init x else Locale.init x;
+fun locale_intern new_locale x =
+  if !new_locales andalso new_locale then NewLocale.intern x else Locale.intern x;
 
 (* context data *)
 
-datatype target = Target of {target: string, is_locale: bool,
+datatype target = Target of {target: string, new_locale: bool, is_locale: bool,
   is_class: bool, instantiation: string list * (string * sort) list * sort,
   overloading: (string * (string * typ) * bool) list};
 
-fun make_target target is_locale is_class instantiation overloading =
-  Target {target = target, is_locale = is_locale,
+fun make_target target new_locale is_locale is_class instantiation overloading =
+  Target {target = target, new_locale = new_locale, is_locale = is_locale,
     is_class = is_class, instantiation = instantiation, overloading = overloading};
 
-val global_target = make_target "" false false ([], [], []) [];
+val global_target = make_target "" false false false ([], [], []) [];
 
 structure Data = ProofDataFun
 (
@@ -58,7 +65,7 @@
 fun pretty_thy ctxt target is_locale is_class =
   let
     val thy = ProofContext.theory_of ctxt;
-    val target_name = (if is_class then "class " else "locale ") ^ locale_extern thy target;
+    val target_name = (if is_class then "class " else "locale ") ^ locale_extern is_class thy target;
     val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
       (#1 (ProofContext.inferred_fixes ctxt));
     val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
@@ -73,7 +80,7 @@
       (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)]
   end;
 
-fun pretty (Target {target, is_locale, is_class, instantiation, overloading}) ctxt =
+fun pretty (Target {target, is_locale, is_class, instantiation, overloading, ...}) ctxt =
   Pretty.block [Pretty.str "theory", Pretty.brk 1,
       Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] ::
     (if not (null overloading) then [Overloading.pretty ctxt]
@@ -83,7 +90,7 @@
 
 (* target declarations *)
 
-fun target_decl add (Target {target, is_class, ...}) d lthy =
+fun target_decl add (Target {target, new_locale, ...}) d lthy =
   let
     val d' = Morphism.transform (LocalTheory.target_morphism lthy) d;
     val d0 = Morphism.form d';
@@ -94,7 +101,7 @@
       |> LocalTheory.target (Context.proof_map d0)
     else
       lthy
-      |> LocalTheory.target (add target d')
+      |> LocalTheory.target (add new_locale target d')
   end;
 
 val type_syntax = target_decl locale_add_type_syntax;
@@ -160,7 +167,7 @@
   |> ProofContext.note_thmss_i kind facts
   ||> ProofContext.restore_naming ctxt;
 
-fun notes (Target {target, is_locale, is_class, ...}) kind facts lthy =
+fun notes (Target {target, is_locale, new_locale, ...}) kind facts lthy =
   let
     val thy = ProofContext.theory_of lthy;
     val facts' = facts
@@ -179,7 +186,7 @@
         #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
         #> Sign.restore_naming thy)
     |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
-    |> is_locale ? LocalTheory.target (locale_add_thmss target kind target_facts)
+    |> is_locale ? LocalTheory.target (locale_add_thmss new_locale target kind target_facts)
     |> note_local kind local_facts
   end;
 
@@ -328,13 +335,14 @@
 
 fun init_target _ NONE = global_target
   | init_target thy (SOME target) =
-      make_target target true (Class.is_class thy target) ([], [], []) [];
+      make_target target (NewLocale.test_locale thy (NewLocale.intern thy target))
+      true (Class.is_class thy target) ([], [], []) [];
 
-fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) =
+fun init_ctxt (Target {target, new_locale, is_locale, is_class, instantiation, overloading}) =
   if not (null (#1 instantiation)) then Class.init_instantiation instantiation
   else if not (null overloading) then Overloading.init overloading
   else if not is_locale then ProofContext.init
-  else if not is_class then locale_init target
+  else if not is_class then locale_init new_locale target
   else Class.init target;
 
 fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
@@ -359,7 +367,7 @@
     val ctxt = ProofContext.init thy;
     val ops = raw_ops |> map (fn (name, const, checked) =>
       (name, Term.dest_Const (prep_const ctxt const), checked));
-  in thy |> init_lthy_ctxt (make_target "" false false ([], [], []) ops) end;
+  in thy |> init_lthy_ctxt (make_target "" false false false ([], [], []) ops) end;
 
 in
 
@@ -367,9 +375,10 @@
 fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt;
 
 fun context "-" thy = init NONE thy
-  | context target thy = init (SOME (locale_intern thy target)) thy;
+  | context target thy = init (SOME (locale_intern
+      (NewLocale.test_locale thy (NewLocale.intern thy target)) thy target)) thy;
 
-fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
+fun instantiation arities = init_lthy_ctxt (make_target "" false false false arities []);
 
 val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
 val overloading_cmd = gen_overloading Syntax.read_term;
diff -r 918687637307 -r 3adc06d6504f src/ZF/Constructible/L_axioms.thy
--- a/src/ZF/Constructible/L_axioms.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/ZF/Constructible/L_axioms.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Constructible/L_axioms.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
@@ -100,7 +99,7 @@
   apply (rule L_nat)
   done
 
-interpretation M_trivial ["L"] by (rule M_trivial_L)
+interpretation L: M_trivial L by (rule M_trivial_L)
 
 (* Replaces the following declarations...
 lemmas rall_abs = M_trivial.rall_abs [OF M_trivial_L]
diff -r 918687637307 -r 3adc06d6504f src/ZF/Constructible/Rec_Separation.thy
--- a/src/ZF/Constructible/Rec_Separation.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Constructible/Rec_Separation.thy
-    ID:   $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
@@ -186,7 +185,7 @@
 theorem M_trancl_L: "PROP M_trancl(L)"
 by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L])
 
-interpretation M_trancl [L] by (rule M_trancl_L)
+interpretation L: M_trancl L by (rule M_trancl_L)
 
 
 subsection{*@{term L} is Closed Under the Operator @{term list}*}
@@ -373,7 +372,7 @@
   apply (rule M_datatypes_axioms_L) 
   done
 
-interpretation M_datatypes [L] by (rule M_datatypes_L)
+interpretation L: M_datatypes L by (rule M_datatypes_L)
 
 
 subsection{*@{term L} is Closed Under the Operator @{term eclose}*}
@@ -436,7 +435,7 @@
   apply (rule M_eclose_axioms_L)
   done
 
-interpretation M_eclose [L] by (rule M_eclose_L)
+interpretation L: M_eclose L by (rule M_eclose_L)
 
 
 end
diff -r 918687637307 -r 3adc06d6504f src/ZF/Constructible/Separation.thy
--- a/src/ZF/Constructible/Separation.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/ZF/Constructible/Separation.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -305,7 +305,7 @@
 theorem M_basic_L: "PROP M_basic(L)"
 by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L])
 
-interpretation M_basic [L] by (rule M_basic_L)
+interpretation L: M_basic L by (rule M_basic_L)
 
 
 end
diff -r 918687637307 -r 3adc06d6504f src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/ZF/ROOT.ML	Thu Dec 18 20:19:49 2008 +0100
@@ -8,5 +8,6 @@
 Paulson.
 *)
 
+set new_locales;
 use_thys ["Main", "Main_ZFC"];
 
diff -r 918687637307 -r 3adc06d6504f src/ZF/ex/Group.thy
--- a/src/ZF/ex/Group.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/ZF/ex/Group.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -1,5 +1,4 @@
 (* Title:  ZF/ex/Group.thy
-  Id:     $Id$
 
 *)
 
@@ -40,7 +39,7 @@
   m_inv :: "i => i => i" ("inv\<index> _" [81] 80) where
   "inv\<^bsub>G\<^esub> x == (THE y. y \<in> carrier(G) & y \<cdot>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub> & x \<cdot>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub>)"
 
-locale monoid = struct G +
+locale monoid = fixes G (structure)
   assumes m_closed [intro, simp]:
          "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> carrier(G)"
       and m_assoc:
@@ -242,7 +241,7 @@
 
 subsection {* Substructures *}
 
-locale subgroup = var H + struct G + 
+locale subgroup = fixes H and G (structure)
   assumes subset: "H \<subseteq> carrier(G)"
     and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> H"
     and  one_closed [simp]: "\<one> \<in> H"
@@ -262,7 +261,7 @@
   assumes "group(G)"
   shows "group_axioms (update_carrier(G,H))"
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   show ?thesis by (force intro: group_axioms.intro l_inv r_inv)
 qed
 
@@ -270,7 +269,7 @@
   assumes "group(G)"
   shows "group (update_carrier(G,H))"
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   show ?thesis
   by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
 qed
@@ -316,8 +315,8 @@
   assumes "group(G)" and "group(H)"
   shows "group (G \<Otimes> H)"
 proof -
-  interpret G: group [G] by fact
-  interpret H: group [H] by fact
+  interpret G: group G by fact
+  interpret H: group H by fact
   show ?thesis by (force intro!: groupI G.m_assoc H.m_assoc G.l_inv H.l_inv
           simp add: DirProdGroup_def)
 qed
@@ -397,8 +396,8 @@
   assumes "group(G)" and "group(H)"
   shows "(\<lambda><x,y> \<in> carrier(G \<Otimes> H). <y,x>) \<in> (G \<Otimes> H) \<cong> (H \<Otimes> G)"
 proof -
-  interpret group [G] by fact
-  interpret group [H] by fact
+  interpret group G by fact
+  interpret group H by fact
   show ?thesis by (auto simp add: iso_def hom_def inj_def surj_def bij_def)
 qed
 
@@ -407,16 +406,17 @@
   shows "(\<lambda><<x,y>,z> \<in> carrier((G \<Otimes> H) \<Otimes> I). <x,<y,z>>)
           \<in> ((G \<Otimes> H) \<Otimes> I) \<cong> (G \<Otimes> (H \<Otimes> I))"
 proof -
-  interpret group [G] by fact
-  interpret group [H] by fact
-  interpret group [I] by fact
+  interpret group G by fact
+  interpret group H by fact
+  interpret group I by fact
   show ?thesis
     by (auto intro: lam_type simp add: iso_def hom_def inj_def surj_def bij_def) 
 qed
 
 text{*Basis for homomorphism proofs: we assume two groups @{term G} and
   @term{H}, with a homomorphism @{term h} between them*}
-locale group_hom = group G + group H + var h +
+locale group_hom = G: group G + H: group H
+  for G (structure) and H (structure) and h +
   assumes homh: "h \<in> hom(G,H)"
   notes hom_mult [simp] = hom_mult [OF homh]
     and hom_closed [simp] = hom_closed [OF homh]
@@ -870,7 +870,7 @@
    assumes "group(G)"
    shows "equiv (carrier(G), rcong H)"
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   show ?thesis proof (simp add: equiv_def, intro conjI)
     show "rcong H \<subseteq> carrier(G) \<times> carrier(G)"
       by (auto simp add: r_congruent_def) 
@@ -907,7 +907,7 @@
   assumes a: "a \<in> carrier(G)"
   shows "a <# H = (rcong H) `` {a}" 
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   show ?thesis
     by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a
       Collect_image_eq) 
@@ -920,7 +920,7 @@
         h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>
       \<Longrightarrow> hb \<cdot> a \<in> (\<Union>h\<in>H. {h \<cdot> b})" (is "PROP ?P")
 proof -
-  interpret subgroup [H G] by fact
+  interpret subgroup H G by fact
   show "PROP ?P"
     apply (rule UN_I [of "hb \<cdot> ((inv ha) \<cdot> h)"], simp)
     apply (simp add: m_assoc transpose_inv)
@@ -931,7 +931,7 @@
   assumes "subgroup(H, G)"
   shows "\<lbrakk>a \<in> rcosets H; b \<in> rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = 0" (is "PROP ?P")
 proof -
-  interpret subgroup [H G] by fact
+  interpret subgroup H G by fact
   show "PROP ?P"
     apply (simp add: RCOSETS_def r_coset_def)
     apply (blast intro: rcos_equation prems sym)
@@ -949,7 +949,7 @@
   assumes "subgroup(H, G)"
   shows "x \<in> carrier(G) \<Longrightarrow> x \<in> H #> x" (is "PROP ?P")
 proof -
-  interpret subgroup [H G] by fact
+  interpret subgroup H G by fact
   show "PROP ?P"
     apply (simp add: r_coset_def)
     apply (rule_tac x="\<one>" in bexI) apply (auto)
@@ -960,7 +960,7 @@
   assumes "subgroup(H, G)"
   shows "\<Union>(rcosets H) = carrier(G)"
 proof -
-  interpret subgroup [H G] by fact
+  interpret subgroup H G by fact
   show ?thesis
     apply (rule equalityI)
     apply (force simp add: RCOSETS_def r_coset_def)
@@ -1044,7 +1044,7 @@
   assumes "group(G)"
   shows "H \<in> rcosets H"
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   have "H #> \<one> = H"
     using _ subgroup_axioms by (rule coset_join2) simp_all
   then show ?thesis
diff -r 918687637307 -r 3adc06d6504f src/ZF/ex/Ring.thy
--- a/src/ZF/ex/Ring.thy	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/ZF/ex/Ring.thy	Thu Dec 18 20:19:49 2008 +0100
@@ -45,7 +45,7 @@
   minus :: "[i,i,i] => i" (infixl "\<ominus>\<index>" 65) where
   "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
 
-locale abelian_monoid = struct G +
+locale abelian_monoid = fixes G (structure)
   assumes a_comm_monoid: 
     "comm_monoid (<carrier(G), add_field(G), zero(G), 0>)"
 
@@ -57,7 +57,7 @@
   assumes a_comm_group: 
     "comm_group (<carrier(G), add_field(G), zero(G), 0>)"
 
-locale ring = abelian_group R + monoid R +
+locale ring = abelian_group R + monoid R for R (structure) +
   assumes l_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
       \<Longrightarrow> (x \<oplus> y) \<cdot> z = x \<cdot> z \<oplus> y \<cdot> z"
     and r_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
@@ -262,7 +262,8 @@
 lemma ring_hom_one: "h \<in> ring_hom(R,S) \<Longrightarrow> h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>"
 by (simp add: ring_hom_def)
 
-locale ring_hom_cring = cring R + cring S + var h +
+locale ring_hom_cring = R: cring R + S: cring S
+  for R (structure) and S (structure) and 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]