# HG changeset patch
# User wenzelm
# Date 1331760858 -3600
# Node ID efb98d27dc1a41dd3e566e68095b2920918d0e89
# Parent  571ce2bc0b64994555273eee440e939e5479a253# Parent  98ffc3fe31cc38c968b27d85d75a7f9636294e0d
merged

diff -r 571ce2bc0b64 -r efb98d27dc1a NEWS
--- a/NEWS	Wed Mar 14 17:19:30 2012 +0000
+++ b/NEWS	Wed Mar 14 22:34:18 2012 +0100
@@ -371,6 +371,12 @@
 
 *** ML ***
 
+* Local_Theory.define no longer hard-wires default theorem name
+"foo_def": definitional packages need to make this explicit, and may
+choose to omit theorem bindings for definitions by using
+Binding.empty/Attrib.empty_binding.  Potential INCOMPATIBILITY for
+derived definitional packages.
+
 * Renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in
 conformance with similar operations in structure Term and Logic.
 
diff -r 571ce2bc0b64 -r efb98d27dc1a src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/HOL/Library/Multiset.thy	Wed Mar 14 22:34:18 2012 +0100
@@ -118,8 +118,8 @@
 lemma count_union [simp]: "count (M + N) a = count M a + count N a"
   by (simp add: union_def in_multiset multiset_typedef)
 
-instance multiset :: (type) cancel_comm_monoid_add proof
-qed (simp_all add: multiset_eq_iff)
+instance multiset :: (type) cancel_comm_monoid_add
+  by default (simp_all add: multiset_eq_iff)
 
 
 subsubsection {* Difference *}
@@ -270,8 +270,8 @@
 definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
   mset_less_def: "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
 
-instance proof
-qed (auto simp add: mset_le_def mset_less_def multiset_eq_iff intro: order_trans antisym)
+instance
+  by default (auto simp add: mset_le_def mset_less_def multiset_eq_iff intro: order_trans antisym)
 
 end
 
@@ -377,10 +377,11 @@
 definition inf_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
   multiset_inter_def: "inf_multiset A B = A - (A - B)"
 
-instance proof -
+instance
+proof -
   have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" by arith
-  show "OFCLASS('a multiset, semilattice_inf_class)" proof
-  qed (auto simp add: multiset_inter_def mset_le_def aux)
+  show "OFCLASS('a multiset, semilattice_inf_class)"
+    by default (auto simp add: multiset_inter_def mset_le_def aux)
 qed
 
 end
@@ -822,7 +823,8 @@
 lemma multiset_of_eq_length:
   assumes "multiset_of xs = multiset_of ys"
   shows "length xs = length ys"
-using assms proof (induct xs arbitrary: ys)
+using assms
+proof (induct xs arbitrary: ys)
   case Nil then show ?case by simp
 next
   case (Cons x xs)
@@ -845,7 +847,8 @@
 next
   case True
   moreover have "z \<in># multiset_of ys" using assms True by simp
-  show ?thesis using assms proof (induct xs arbitrary: ys)
+  show ?thesis using assms
+  proof (induct xs arbitrary: ys)
     case Nil then show ?case by simp
   next
     case (Cons x xs)
@@ -864,7 +867,8 @@
   assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
     and equiv: "multiset_of xs = multiset_of ys"
   shows "fold f xs = fold f ys"
-using f equiv [symmetric] proof (induct xs arbitrary: ys)
+using f equiv [symmetric]
+proof (induct xs arbitrary: ys)
   case Nil then show ?case by simp
 next
   case (Cons x xs)
@@ -898,7 +902,8 @@
   and "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>x. f k = f x) ys = filter (\<lambda>x. f k = f x) xs"
   and "sorted (map f ys)"
   shows "sort_key f xs = ys"
-using assms proof (induct xs arbitrary: ys)
+using assms
+proof (induct xs arbitrary: ys)
   case Nil then show ?case by simp
 next
   case (Cons x xs)
@@ -994,10 +999,12 @@
 proof (cases xs)
   case Nil then show ?thesis by simp
 next
-  case (Cons _ ys) note hyps = Cons show ?thesis proof (cases ys)
+  case (Cons _ ys) note hyps = Cons show ?thesis
+  proof (cases ys)
     case Nil with hyps show ?thesis by simp
   next
-    case (Cons _ zs) note hyps = hyps Cons show ?thesis proof (cases zs)
+    case (Cons _ zs) note hyps = hyps Cons show ?thesis
+    proof (cases zs)
       case Nil with hyps show ?thesis by auto
     next
       case Cons 
@@ -1224,8 +1231,8 @@
 definition
   [code]: "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
 
-instance proof
-qed (simp add: equal_multiset_def eq_iff)
+instance
+  by default (simp add: equal_multiset_def eq_iff)
 
 end
 
@@ -1512,8 +1519,8 @@
   qed
   have trans: "\<And>K M N :: 'a multiset. K \<subset># M \<Longrightarrow> M \<subset># N \<Longrightarrow> K \<subset># N"
     unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
-  show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
-  qed (auto simp add: le_multiset_def irrefl dest: trans)
+  show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset"
+    by default (auto simp add: le_multiset_def irrefl dest: trans)
 qed
 
 lemma mult_less_irrefl [elim!]: "M \<subset># (M::'a::order multiset) ==> R"
@@ -1785,14 +1792,12 @@
 
 enriched_type image_mset: image_mset
 proof -
-  fix f g 
-  show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
+  fix f g show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
   proof
     fix A
     show "(image_mset f \<circ> image_mset g) A = image_mset (f \<circ> g) A"
       by (induct A) simp_all
   qed
-next
   show "image_mset id = id"
   proof
     fix A
diff -r 571ce2bc0b64 -r efb98d27dc1a src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/HOL/Statespace/state_space.ML	Wed Mar 14 22:34:18 2012 +0100
@@ -15,7 +15,7 @@
   val namespace_definition :
      bstring ->
      typ ->
-     Expression.expression ->
+     (xstring, string) Expression.expr * (binding * string option * mixfix) list ->
      string list -> string list -> theory -> theory
 
   val define_statespace :
@@ -139,9 +139,12 @@
 
 val get_silent = #silent o NameSpaceData.get;
 
+fun expression_no_pos (expr, fixes) : Expression.expression =
+  (map (fn (name, inst) => ((name, Position.none), inst)) expr, fixes);
+
 fun prove_interpretation_in ctxt_tac (name, expr) thy =
    thy
-   |> Expression.sublocale_cmd I name expr []
+   |> Expression.sublocale_cmd I (name, Position.none) (expression_no_pos expr) []
    |> Proof.global_terminal_proof
          (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), NONE)
    |> Proof_Context.theory_of
@@ -154,7 +157,7 @@
 
 fun add_locale_cmd name expr elems thy =
   thy
-  |> Expression.add_locale_cmd I (Binding.name name) Binding.empty expr elems
+  |> Expression.add_locale_cmd I (Binding.name name) Binding.empty (expression_no_pos expr) elems
   |> snd
   |> Local_Theory.exit;
 
diff -r 571ce2bc0b64 -r efb98d27dc1a src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/HOL/Tools/inductive.ML	Wed Mar 14 22:34:18 2012 +0100
@@ -562,9 +562,12 @@
 fun gen_inductive_cases prep_att prep_prop args lthy =
   let
     val thy = Proof_Context.theory_of lthy;
-    val facts = args |> grouped 10 Par_List.map (fn ((a, atts), props) =>
-      ((a, map (prep_att thy) atts),
-        map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
+    val thmss =
+      map snd args
+      |> burrow (grouped 10 Par_List.map (mk_cases lthy o prep_prop lthy));
+    val facts =
+      map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att thy) atts), [(thms, [])]))
+        args thmss;
   in lthy |> Local_Theory.notes facts |>> map snd end;
 
 val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
@@ -809,7 +812,7 @@
       |> Local_Theory.conceal
       |> Local_Theory.define
         ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
-         ((Binding.empty, @{attributes [nitpick_unfold]}),
+         ((Thm.def_binding rec_name, @{attributes [nitpick_unfold]}),
            fold_rev lambda params
              (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
       ||> Local_Theory.restore_naming lthy;
diff -r 571ce2bc0b64 -r efb98d27dc1a src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/class.ML	Wed Mar 14 22:34:18 2012 +0100
@@ -37,7 +37,6 @@
     -> (Proof.context -> 'b -> tactic) -> 'a -> local_theory -> 'b * theory
   val read_multi_arity: theory -> xstring list * xstring list * xstring
     -> string list * (string * sort) list * sort
-  val type_name: string -> string
   val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
   val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
 
@@ -57,7 +56,7 @@
 
 (** class data **)
 
-datatype class_data = ClassData of {
+datatype class_data = Class_Data of {
 
   (* static part *)
   consts: (string * string) list
@@ -78,23 +77,23 @@
 
 fun make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
     (defs, operations)) =
-  ClassData { consts = consts, base_sort = base_sort,
+  Class_Data {consts = consts, base_sort = base_sort,
     base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
-    of_class = of_class, axiom = axiom, defs = defs, operations = operations };
-fun map_class_data f (ClassData { consts, base_sort, base_morph, export_morph, assm_intro,
-    of_class, axiom, defs, operations }) =
+    of_class = of_class, axiom = axiom, defs = defs, operations = operations};
+fun map_class_data f (Class_Data {consts, base_sort, base_morph, export_morph, assm_intro,
+    of_class, axiom, defs, operations}) =
   make_class_data (f ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
     (defs, operations)));
-fun merge_class_data _ (ClassData { consts = consts,
+fun merge_class_data _ (Class_Data {consts = consts,
     base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
-    of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
-  ClassData { consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _,
-    of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
+    of_class = of_class, axiom = axiom, defs = defs1, operations = operations1},
+  Class_Data {consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _,
+    of_class = _, axiom = _, defs = defs2, operations = operations2}) =
   make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
     (Thm.merge_thms (defs1, defs2),
       AList.merge (op =) (K true) (operations1, operations2)));
 
-structure ClassData = Theory_Data
+structure Class_Data = Theory_Data
 (
   type T = class_data Graph.T
   val empty = Graph.empty;
@@ -105,18 +104,20 @@
 
 (* queries *)
 
-fun lookup_class_data thy class = case try (Graph.get_node (ClassData.get thy)) class
- of SOME (ClassData data) => SOME data
-  | NONE => NONE;
+fun lookup_class_data thy class =
+  (case try (Graph.get_node (Class_Data.get thy)) class of
+    SOME (Class_Data data) => SOME data
+  | NONE => NONE);
 
-fun the_class_data thy class = case lookup_class_data thy class
- of NONE => error ("Undeclared class " ^ quote class)
-  | SOME data => data;
+fun the_class_data thy class =
+  (case lookup_class_data thy class of
+    NONE => error ("Undeclared class " ^ quote class)
+  | SOME data => data);
 
 val is_class = is_some oo lookup_class_data;
 
-val ancestry = Graph.all_succs o ClassData.get;
-val heritage = Graph.all_preds o ClassData.get;
+val ancestry = Graph.all_succs o Class_Data.get;
+val heritage = Graph.all_preds o Class_Data.get;
 
 fun these_params thy =
   let
@@ -133,20 +134,21 @@
 val base_sort = #base_sort oo the_class_data;
 
 fun rules thy class =
-  let val { axiom, of_class, ... } = the_class_data thy class
+  let val {axiom, of_class, ...} = the_class_data thy class
   in (axiom, of_class) end;
 
 fun all_assm_intros thy =
-  Graph.fold (fn (_, (ClassData { assm_intro, ... }, _)) => fold (insert Thm.eq_thm)
-    (the_list assm_intro)) (ClassData.get thy) [];
+  Graph.fold (fn (_, (Class_Data {assm_intro, ...}, _)) => fold (insert Thm.eq_thm)
+    (the_list assm_intro)) (Class_Data.get thy) [];
 
 fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy;
 fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy;
 
 val base_morphism = #base_morph oo the_class_data;
-fun morphism thy class = case Element.eq_morphism thy (these_defs thy [class])
- of SOME eq_morph => base_morphism thy class $> eq_morph
-  | NONE => base_morphism thy class;
+fun morphism thy class =
+  (case Element.eq_morphism thy (these_defs thy [class]) of
+    SOME eq_morph => base_morphism thy class $> eq_morph
+  | NONE => base_morphism thy class);
 val export_morphism = #export_morph oo the_class_data;
 
 fun print_classes ctxt =
@@ -195,13 +197,14 @@
         make_class_data (((map o pairself) fst params, base_sort,
           base_morph, export_morph, assm_intro, of_class, axiom), ([], operations)))
       #> fold (curry Graph.add_edge class) sups;
-  in ClassData.map add_class thy end;
+  in Class_Data.map add_class thy end;
 
-fun activate_defs class thms thy = case Element.eq_morphism thy thms
- of SOME eq_morph => fold (fn cls => fn thy =>
+fun activate_defs class thms thy =
+  (case Element.eq_morphism thy thms of
+    SOME eq_morph => fold (fn cls => fn thy =>
       Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls)
         (eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy
-  | NONE => thy;
+  | NONE => thy);
 
 fun register_operation class (c, (t, some_def)) thy =
   let
@@ -213,7 +216,7 @@
     val ty' = Term.fastype_of t';
   in
     thy
-    |> (ClassData.map o Graph.map_node class o map_class_data o apsnd)
+    |> (Class_Data.map o Graph.map_node class o map_class_data o apsnd)
       (fn (defs, operations) =>
         (fold cons (the_list some_def) defs,
           (c, (class, (ty', t'))) :: operations))
@@ -231,14 +234,15 @@
     val diff_sort = Sign.complete_sort thy [sup]
       |> subtract (op =) (Sign.complete_sort thy [sub])
       |> filter (is_class thy);
-    val add_dependency = case some_dep_morph
-     of SOME dep_morph => Locale.add_dependency sub
+    val add_dependency =
+      (case some_dep_morph of
+        SOME dep_morph => Locale.add_dependency sub
           (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) NONE export
-      | NONE => I
+      | NONE => I);
   in
     thy
     |> AxClass.add_classrel classrel
-    |> ClassData.map (Graph.add_edge (sub, sup))
+    |> Class_Data.map (Graph.add_edge (sub, sup))
     |> activate_defs sub (these_defs thy diff_sort)
     |> add_dependency
   end;
@@ -265,17 +269,19 @@
       (map o apsnd) (subst_class_typ base_sort o fst o snd) operations;
     val secondary_constraints =
       (map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations;
-    fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c
-     of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty
-         of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
-             of SOME (_, ty' as TVar (vi, sort)) =>
-                  if Type_Infer.is_param vi
-                    andalso Sorts.sort_le algebra (base_sort, sort)
-                      then SOME (ty', TFree (Name.aT, base_sort))
-                      else NONE
+    fun improve (c, ty) =
+      (case AList.lookup (op =) primary_constraints c of
+        SOME ty' =>
+          (case try (Type.raw_match (ty', ty)) Vartab.empty of
+            SOME tyenv =>
+              (case Vartab.lookup tyenv (Name.aT, 0) of
+                SOME (_, ty' as TVar (vi, sort)) =>
+                  if Type_Infer.is_param vi andalso Sorts.sort_le algebra (base_sort, sort)
+                  then SOME (ty', TFree (Name.aT, base_sort))
+                  else NONE
               | _ => NONE)
           | NONE => NONE)
-      | NONE => NONE)
+      | NONE => NONE);
     fun subst (c, ty) = Option.map snd (AList.lookup (op =) operations c);
     val unchecks = these_unchecks thy sort;
   in
@@ -398,20 +404,24 @@
 
 structure Instantiation = Proof_Data
 (
-  type T = instantiation
-  fun init _ = Instantiation { arities = ([], [], []), params = [] };
+  type T = instantiation;
+  fun init _ = Instantiation {arities = ([], [], []), params = []};
 );
 
 fun mk_instantiation (arities, params) =
-  Instantiation { arities = arities, params = params };
-fun get_instantiation lthy = case Instantiation.get (Local_Theory.target_of lthy)
- of Instantiation data => data;
-fun map_instantiation f = (Local_Theory.target o Instantiation.map)
-  (fn Instantiation { arities, params } => mk_instantiation (f (arities, params)));
+  Instantiation {arities = arities, params = params};
+
+val get_instantiation =
+  (fn Instantiation data => data) o Instantiation.get o Local_Theory.target_of;
 
-fun the_instantiation lthy = case get_instantiation lthy
- of { arities = ([], [], []), ... } => error "No instantiation target"
-  | data => data;
+fun map_instantiation f =
+  (Local_Theory.target o Instantiation.map)
+    (fn Instantiation {arities, params} => mk_instantiation (f (arities, params)));
+
+fun the_instantiation lthy =
+  (case get_instantiation lthy of
+    {arities = ([], [], []), ...} => error "No instantiation target"
+  | data => data);
 
 val instantiation_params = #params o get_instantiation;
 
@@ -434,20 +444,21 @@
 
 fun synchronize_inst_syntax ctxt =
   let
-    val Instantiation { params, ... } = Instantiation.get ctxt;
+    val Instantiation {params, ...} = Instantiation.get ctxt;
 
     val lookup_inst_param = AxClass.lookup_inst_param
       (Sign.consts_of (Proof_Context.theory_of ctxt)) params;
-    fun subst (c, ty) = case lookup_inst_param (c, ty)
-     of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
-      | NONE => NONE;
+    fun subst (c, ty) =
+      (case lookup_inst_param (c, ty) of
+        SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
+      | NONE => NONE);
     val unchecks =
       map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params;
   in
     ctxt
     |> Overloading.map_improvable_syntax
-         (fn (((primary_constraints, _), (((improve, _), _), _)), _) =>
-            (((primary_constraints, []), (((improve, subst), false), unchecks)), false))
+      (fn (((primary_constraints, _), (((improve, _), _), _)), _) =>
+          (((primary_constraints, []), (((improve, subst), false), unchecks)), false))
   end;
 
 fun resort_terms ctxt algebra consts constraints ts =
@@ -467,53 +478,35 @@
 
 (* target *)
 
-val sanitize_name = (*necessary as long as "dirty" type identifiers are permitted*)
-  let
-    fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s
-      orelse s = "'" orelse s = "_";
-    val is_junk = not o is_valid andf Symbol.is_regular;
-    val junk = Scan.many is_junk;
-    val scan_valids = Symbol.scanner "Malformed input"
-      ((junk |--
-        (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
-        --| junk))
-      ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
-  in
-    raw_explode #> scan_valids #> implode
-  end;
-
-val type_name = sanitize_name o Long_Name.base_name;
-
 fun define_overloaded (c, U) v (b_def, rhs) = Local_Theory.background_theory_result
     (AxClass.declare_overloaded (c, U) ##>> AxClass.define_overloaded b_def (c, rhs))
   ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
   ##> Local_Theory.target synchronize_inst_syntax;
 
 fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
-  case instantiation_param lthy b
-   of SOME c => if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
-        else lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
-    | NONE => lthy |>
-        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
+  (case instantiation_param lthy b of
+    SOME c =>
+      if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
+      else lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
+  | NONE => lthy |>
+      Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params));
 
 fun pretty lthy =
   let
-    val { arities = (tycos, vs, sort), params } = the_instantiation lthy;
+    val {arities = (tycos, vs, sort), params} = the_instantiation lthy;
     fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
     fun pr_param ((c, _), (v, ty)) =
       Pretty.block (Pretty.breaks
         [Pretty.str v, Pretty.str "==", Pretty.str (Proof_Context.extern_const lthy c),
           Pretty.str "::", Syntax.pretty_typ lthy ty]);
-  in Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params end;
+  in Pretty.command "instantiation" :: map pr_arity tycos @ map pr_param params end;
 
 fun conclude lthy =
   let
     val (tycos, vs, sort) = #arities (the_instantiation lthy);
     val thy = Proof_Context.theory_of lthy;
     val _ = tycos |> List.app (fn tyco =>
-      if Sign.of_sort thy
-        (Type (tyco, map TFree vs), sort)
-      then ()
+      if Sign.of_sort thy (Type (tyco, map TFree vs), sort) then ()
       else error ("Missing instance proof for type " ^ quote (Proof_Context.extern_type lthy tyco)));
   in lthy end;
 
@@ -524,7 +517,7 @@
     fun get_param tyco (param, (_, (c, ty))) =
       if can (AxClass.param_of_inst thy) (c, tyco)
       then NONE else SOME ((c, tyco),
-        (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
+        (param ^ "_" ^ Long_Name.base_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
     val params = map_product get_param tycos class_params |> map_filter I;
     val primary_constraints = map (apsnd
       (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
diff -r 571ce2bc0b64 -r efb98d27dc1a src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/class_declaration.ML	Wed Mar 14 22:34:18 2012 +0100
@@ -198,10 +198,11 @@
 
 fun prep_class_spec prep_class prep_class_elems thy raw_supclasses raw_elems =
   let
+    val thy_ctxt = Proof_Context.init_global thy;
 
     (* prepare import *)
     val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy));
-    val sups = Sign.minimize_sort thy (map (prep_class thy) raw_supclasses);
+    val sups = Sign.minimize_sort thy (map (prep_class thy_ctxt) raw_supclasses);
     val _ =
       (case filter_out (Class.is_class thy) sups of
         [] => ()
@@ -219,7 +220,7 @@
     val sup_sort = inter_sort base_sort sups;
 
     (* process elements as class specification *)
-    val class_ctxt = Class.begin sups base_sort (Proof_Context.init_global thy);
+    val class_ctxt = Class.begin sups base_sort thy_ctxt;
     val ((_, _, syntax_elems), _) = class_ctxt
       |> Expression.cert_declaration supexpr I inferred_elems;
     fun check_vars e vs =
@@ -243,7 +244,7 @@
   in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (elems, global_syntax)) end;
 
 val cert_class_spec = prep_class_spec (K I) cert_class_elems;
-val read_class_spec = prep_class_spec Sign.intern_class read_class_elems;
+val read_class_spec = prep_class_spec Proof_Context.read_class read_class_elems;
 
 
 (* class establishment *)
diff -r 571ce2bc0b64 -r efb98d27dc1a src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/expression.ML	Wed Mar 14 22:34:18 2012 +0100
@@ -8,9 +8,9 @@
 sig
   (* Locale expressions *)
   datatype 'term map = Positional of 'term option list | Named of (string * 'term) list
-  type 'term expr = (string * ((string * bool) * 'term map)) list
-  type expression_i = term expr * (binding * typ option * mixfix) list
-  type expression = string expr * (binding * string option * mixfix) list
+  type ('name, 'term) expr = ('name * ((string * bool) * 'term map)) list
+  type expression_i = (string, term) expr * (binding * typ option * mixfix) list
+  type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list
 
   (* Processing of context statements *)
   val cert_statement: Element.context_i list -> (term * term list) list list ->
@@ -41,7 +41,7 @@
     (term list list * (string * morphism) list * morphism) * Proof.context
   val sublocale: (local_theory -> local_theory) -> string -> expression_i ->
     (Attrib.binding * term) list -> theory -> Proof.state
-  val sublocale_cmd: (local_theory -> local_theory) -> string -> expression ->
+  val sublocale_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression ->
     (Attrib.binding * string) list -> theory -> Proof.state
   val interpretation: expression_i -> (Attrib.binding * term) list ->
     theory -> Proof.state
@@ -68,15 +68,15 @@
   Positional of 'term option list |
   Named of (string * 'term) list;
 
-type 'term expr = (string * ((string * bool) * 'term map)) list;
+type ('name, 'term) expr = ('name * ((string * bool) * 'term map)) list;
 
-type expression = string expr * (binding * string option * mixfix) list;
-type expression_i = term expr * (binding * typ option * mixfix) list;
+type expression_i = (string, term) expr * (binding * typ option * mixfix) list;
+type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list;
 
 
 (** Internalise locale names in expr **)
 
-fun intern thy instances =  map (apfst (Locale.intern thy)) instances;
+fun check_expr thy instances = map (apfst (Locale.check thy)) instances;
 
 
 (** Parameters of expression **)
@@ -343,7 +343,8 @@
 
 local
 
-fun prep_full_context_statement parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
+fun prep_full_context_statement
+    parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
     {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_concl ctxt1 =
   let
     val thy = Proof_Context.theory_of ctxt1;
@@ -417,7 +418,7 @@
 
 fun read_full_context_statement x =
   prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_vars
-  parse_inst Proof_Context.read_vars intern x;
+  parse_inst Proof_Context.read_vars check_expr x;
 
 end;
 
@@ -903,10 +904,10 @@
           export thy) (deps ~~ witss))
   end;
 
-fun gen_sublocale prep_expr intern parse_prop prep_attr
+fun gen_sublocale prep_expr prep_loc parse_prop prep_attr
     before_exit raw_target expression equations thy =
   let
-    val target = intern thy raw_target;
+    val target = prep_loc thy raw_target;
     val target_ctxt = Named_Target.init before_exit target thy;
     val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt;
     val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
@@ -923,7 +924,7 @@
 
 fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) (K I) x;
 fun sublocale_cmd x =
-  gen_sublocale read_goal_expression Locale.intern Syntax.parse_prop Attrib.intern_src x;
+  gen_sublocale read_goal_expression Locale.check Syntax.parse_prop Attrib.intern_src x;
 
 end;
 
diff -r 571ce2bc0b64 -r efb98d27dc1a src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/generic_target.ML	Wed Mar 14 22:34:18 2012 +0100
@@ -48,13 +48,11 @@
 
 (* define *)
 
-fun define foundation ((b, mx), ((proto_b_def, atts), rhs)) lthy =
+fun define foundation ((b, mx), ((b_def, atts), rhs)) lthy =
   let
     val thy = Proof_Context.theory_of lthy;
     val thy_ctxt = Proof_Context.init_global thy;
 
-    val b_def = Thm.def_binding_optional b proto_b_def;
-
     (*term and type parameters*)
     val crhs = Thm.cterm_of thy rhs;
     val ((defs, _), rhs') = Local_Defs.export_cterm lthy thy_ctxt crhs ||> Thm.term_of;
@@ -202,7 +200,8 @@
     val lhs = list_comb (const, type_params @ term_params);
     val ((_, def), lthy3) = lthy2
       |> Local_Theory.background_theory_result
-        (Thm.add_def lthy2 false false (b_def, Logic.mk_equals (lhs, rhs)));
+        (Thm.add_def lthy2 false false
+          (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
   in ((lhs, def), lthy3) end;
 
 fun theory_notes kind global_facts lthy =
diff -r 571ce2bc0b64 -r efb98d27dc1a src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Mar 14 22:34:18 2012 +0100
@@ -50,8 +50,8 @@
   val print_configs: Toplevel.transition -> Toplevel.transition
   val print_theorems: bool -> Toplevel.transition -> Toplevel.transition
   val print_locales: Toplevel.transition -> Toplevel.transition
-  val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition
-  val print_registrations: string -> Toplevel.transition -> Toplevel.transition
+  val print_locale: bool * (xstring * Position.T) -> Toplevel.transition -> Toplevel.transition
+  val print_registrations: xstring * Position.T -> Toplevel.transition -> Toplevel.transition
   val print_dependencies: bool * Expression.expression -> Toplevel.transition
     -> Toplevel.transition
   val print_attributes: Toplevel.transition -> Toplevel.transition
diff -r 571ce2bc0b64 -r efb98d27dc1a src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/isar_syn.ML	Wed Mar 14 22:34:18 2012 +0100
@@ -91,13 +91,13 @@
 val _ =
   Outer_Syntax.command "classes" "declare type classes" Keyword.thy_decl
     (Scan.repeat1 (Parse.binding -- Scan.optional ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |--
-        Parse.!!! (Parse.list1 Parse.xname)) [])
+        Parse.!!! (Parse.list1 Parse.class)) [])
       >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
 
 val _ =
   Outer_Syntax.command "classrel" "state inclusion of type classes (axiomatic!)" Keyword.thy_decl
-    (Parse.and_list1 (Parse.xname -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<")
-        |-- Parse.!!! Parse.xname))
+    (Parse.and_list1 (Parse.class -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<")
+        |-- Parse.!!! Parse.class))
     >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
 
 val _ =
@@ -421,7 +421,7 @@
 val _ =
   Outer_Syntax.command "sublocale"
     "prove sublocale relation between a locale and a locale expression" Keyword.thy_goal
-    (Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
+    (Parse.position Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
       parse_interpretation_arguments false
       >> (fn (loc, (expr, equations)) =>
           Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd I loc expr equations)));
@@ -445,7 +445,7 @@
 (* classes *)
 
 val class_val =
-  Parse_Spec.class_expr --
+  Parse_Spec.class_expression --
     Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
   Scan.repeat1 Parse_Spec.context_element >> pair [];
 
@@ -458,7 +458,7 @@
 
 val _ =
   Outer_Syntax.local_theory_to_proof "subclass" "prove a subclass relation" Keyword.thy_goal
-    (Parse.xname >> Class_Declaration.subclass_cmd I);
+    (Parse.class >> Class_Declaration.subclass_cmd I);
 
 val _ =
   Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
@@ -468,8 +468,8 @@
 
 val _ =
   Outer_Syntax.command "instance" "prove type arity or subclass relation" Keyword.thy_goal
-  ((Parse.xname -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.xname)
-        >> Class.classrel_cmd ||
+  ((Parse.class --
+    ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
     Parse.multi_arity >> Class.instance_arity_cmd)
     >> (Toplevel.print oo Toplevel.theory_to_proof) ||
     Scan.succeed
@@ -831,12 +831,12 @@
 
 val _ =
   Outer_Syntax.improper_command "print_locale" "print locale of this theory" Keyword.diag
-    (opt_bang -- Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_locale));
+    (opt_bang -- Parse.position Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_locale));
 
 val _ =
   Outer_Syntax.improper_command "print_interps"
     "print interpretations of locale for this theory or proof context" Keyword.diag
-    (Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
+    (Parse.position Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
 
 val _ =
   Outer_Syntax.improper_command "print_dependencies"
diff -r 571ce2bc0b64 -r efb98d27dc1a src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/keyword.ML	Wed Mar 14 22:34:18 2012 +0100
@@ -32,7 +32,6 @@
   val prf_asm_goal: T
   val prf_script: T
   val kinds: string list
-  val update_tags: string -> string list -> string list
   val tag: string -> T -> T
   val tags_of: T -> string list
   val tag_theory: T -> T
@@ -108,9 +107,7 @@
 
 (* tags *)
 
-fun update_tags t ts = t :: remove (op = : string * string -> bool) t ts;
-
-fun tag t (Keyword (s, ts)) = Keyword (s, update_tags t ts);
+fun tag t (Keyword (s, ts)) = Keyword (s, update (op =) t ts);
 fun tags_of (Keyword (_, ts)) = ts;
 
 val tag_theory = tag "theory";
diff -r 571ce2bc0b64 -r efb98d27dc1a src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/locale.ML	Wed Mar 14 22:34:18 2012 +0100
@@ -79,8 +79,8 @@
   (* Diagnostic *)
   val all_locales: theory -> string list
   val print_locales: theory -> unit
-  val print_locale: theory -> bool -> xstring -> unit
-  val print_registrations: Proof.context -> string -> unit
+  val print_locale: theory -> bool -> xstring * Position.T -> unit
+  val print_registrations: Proof.context -> xstring * Position.T -> unit
   val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> unit
   val locale_deps: theory ->
     {params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list} Graph.T
@@ -618,7 +618,7 @@
 
 fun print_locale thy show_facts raw_name =
   let
-    val name = intern thy raw_name;
+    val name = check thy raw_name;
     val ctxt = init name thy;
     fun cons_elem (elem as Notes _) = show_facts ? cons elem
       | cons_elem elem = cons elem;
@@ -633,8 +633,7 @@
 fun print_registrations ctxt raw_name =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val name = intern thy raw_name;
-    val _ = the_locale thy name;  (* error if locale unknown *)
+    val name = check thy raw_name;
   in
     (case registrations_of (Context.Proof ctxt) (* FIXME *) name of
       [] => Pretty.str "no interpretations"
diff -r 571ce2bc0b64 -r efb98d27dc1a src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/overloading.ML	Wed Mar 14 22:34:18 2012 +0100
@@ -147,15 +147,16 @@
   in 
     ctxt
     |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
-  end
+  end;
 
 fun define_overloaded (c, U) (v, checked) (b_def, rhs) =
   Local_Theory.background_theory_result
     (Thm.add_def_global (not checked) true
-      (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
+      (Thm.def_binding_optional (Binding.name v) b_def,
+        Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
   ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v))
   ##> Local_Theory.target synchronize_syntax
-  #-> (fn (_, def) => pair (Const (c, U), def))
+  #-> (fn (_, def) => pair (Const (c, U), def));
 
 fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   (case operation lthy b of
@@ -173,7 +174,7 @@
       Pretty.block (Pretty.breaks
         [Pretty.str v, Pretty.str "==", Pretty.str (Proof_Context.extern_const lthy c),
           Pretty.str "::", Syntax.pretty_typ lthy ty]);
-  in Pretty.str "overloading" :: map pr_operation overloading end;
+  in Pretty.command "overloading" :: map pr_operation overloading end;
 
 fun conclude lthy =
   let
diff -r 571ce2bc0b64 -r efb98d27dc1a src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/parse.ML	Wed Mar 14 22:34:18 2012 +0100
@@ -69,7 +69,9 @@
   val liberal_name: xstring parser
   val parname: string parser
   val parbinding: binding parser
+  val class: string parser
   val sort: string parser
+  val type_const: string parser
   val arity: (string * string list * string) parser
   val multi_arity: (string list * string list * string) parser
   val type_args: string list parser
@@ -93,7 +95,6 @@
   val prop_group: string parser
   val term: string parser
   val prop: string parser
-  val type_const: string parser
   val const: string parser
   val literal_fact: string parser
   val propp: (string * string list) parser
@@ -257,14 +258,18 @@
 val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty;
 
 
-(* sorts and arities *)
+(* type classes *)
+
+val class = group (fn () => "type class") (inner_syntax xname);
 
 val sort = group (fn () => "sort") (inner_syntax xname);
 
-val arity = xname -- ($$$ "::" |-- !!!
+val type_const = inner_syntax (group (fn () => "type constructor") xname);
+
+val arity = type_const -- ($$$ "::" |-- !!!
   (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
 
-val multi_arity = and_list1 xname -- ($$$ "::" |-- !!!
+val multi_arity = and_list1 type_const -- ($$$ "::" |-- !!!
   (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
 
 
@@ -343,7 +348,6 @@
 val term = inner_syntax term_group;
 val prop = inner_syntax prop_group;
 
-val type_const = inner_syntax (group (fn () => "type constructor") xname);
 val const = inner_syntax (group (fn () => "constant") xname);
 
 val literal_fact = inner_syntax (group (fn () => "literal fact") alt_string);
diff -r 571ce2bc0b64 -r efb98d27dc1a src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/parse_spec.ML	Wed Mar 14 22:34:18 2012 +0100
@@ -22,7 +22,7 @@
   val locale_mixfix: mixfix parser
   val locale_fixes: (binding * string option * mixfix) list parser
   val locale_insts: (string option list * (Attrib.binding * string) list) parser
-  val class_expr: string list parser
+  val class_expression: string list parser
   val locale_expression: bool -> Expression.expression parser
   val locale_keyword: string parser
   val context_element: Element.context parser
@@ -125,11 +125,11 @@
   Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
   Parse.$$$ "defines" || Parse.$$$ "notes";
 
-val class_expr = plus1_unless locale_keyword Parse.xname;
+val class_expression = plus1_unless locale_keyword Parse.class;
 
 fun locale_expression mandatory =
   let
-    val expr2 = Parse.xname;
+    val expr2 = Parse.position Parse.xname;
     val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
       Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
     val expr0 = plus1_unless locale_keyword expr1;
diff -r 571ce2bc0b64 -r efb98d27dc1a src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/proof_context.ML	Wed Mar 14 22:34:18 2012 +0100
@@ -55,8 +55,6 @@
   val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
   val pretty_fact: Proof.context -> string * thm list -> Pretty.T
   val read_class: Proof.context -> xstring -> class
-  val read_arity: Proof.context -> xstring * string list * string -> arity
-  val cert_arity: Proof.context -> arity -> arity
   val read_typ: Proof.context -> string -> typ
   val read_typ_syntax: Proof.context -> string -> typ
   val read_typ_abbrev: Proof.context -> string -> typ
@@ -70,6 +68,8 @@
   val read_type_name_proper: Proof.context -> bool -> string -> typ
   val read_const_proper: Proof.context -> bool -> string -> term
   val read_const: Proof.context -> bool -> typ -> string -> term
+  val read_arity: Proof.context -> xstring * string list * string -> arity
+  val cert_arity: Proof.context -> arity -> arity
   val allow_dummies: Proof.context -> Proof.context
   val prepare_sorts: Proof.context -> typ list -> typ list
   val check_tfree: Proof.context -> string * sort -> string * sort
@@ -367,22 +367,6 @@
   in c end;
 
 
-(* type arities *)
-
-local
-
-fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
-  let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
-  in Type.add_arity ctxt arity (tsig_of ctxt); arity end;
-
-in
-
-val read_arity = prep_arity intern_type Syntax.read_sort;
-val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
-
-end;
-
-
 (* types *)
 
 fun read_typ_mode mode ctxt s =
@@ -504,6 +488,23 @@
 end;
 
 
+(* type arities *)
+
+local
+
+fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
+  let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
+  in Type.add_arity ctxt arity (tsig_of ctxt); arity end;
+
+in
+
+val read_arity =
+  prep_arity (fn ctxt => #1 o dest_Type o read_type_name_proper ctxt true) Syntax.read_sort;
+val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
+
+end;
+
+
 (* skolem variables *)
 
 fun intern_skolem ctxt x =
diff -r 571ce2bc0b64 -r efb98d27dc1a src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Thy/thy_output.ML	Wed Mar 14 22:34:18 2012 +0100
@@ -291,7 +291,7 @@
     val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
 
     val (tag, tags) = tag_stack;
-    val tag' = try hd (fold Keyword.update_tags cmd_tags (the_list tag));
+    val tag' = try hd (fold (update (op =)) cmd_tags (the_list tag));
 
     val active_tag' =
       if is_some tag' then tag'
@@ -586,7 +586,7 @@
     basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
     basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #>
     basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
-    basic_entity (Binding.name "class") (Scan.lift Args.name) pretty_class #>
+    basic_entity (Binding.name "class") (Scan.lift Args.name_source) pretty_class #>
     basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
     basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
     basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
diff -r 571ce2bc0b64 -r efb98d27dc1a src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Mar 14 22:34:18 2012 +0100
@@ -61,12 +61,15 @@
   /* header */
 
   def node_header(): Document.Node_Header =
-    Isabelle.swing_buffer_lock(buffer) {
+  {
+    Swing_Thread.require()
+    Isabelle.buffer_lock(buffer) {
       Exn.capture {
         Isabelle.thy_load.check_header(name,
           Thy_Header.read(buffer.getSegment(0, buffer.getLength)))
       }
     }
+  }
 
 
   /* perspective */
diff -r 571ce2bc0b64 -r efb98d27dc1a src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Mar 14 22:34:18 2012 +0100
@@ -233,13 +233,15 @@
 
   private val mouse_motion_listener = new MouseMotionAdapter {
     override def mouseMoved(e: MouseEvent) {
+      Swing_Thread.assert()
+
       control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
       val x = e.getX()
       val y = e.getY()
 
       if (!model.buffer.isLoaded) exit_control()
       else
-        Isabelle.swing_buffer_lock(model.buffer) {
+        Isabelle.buffer_lock(model.buffer) {
           val snapshot = update_snapshot()
 
           if (control) init_popup(snapshot, x, y)
@@ -284,13 +286,15 @@
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       robust_body(()) {
+        Swing_Thread.assert()
+
         val gutter = text_area.getGutter
         val width = GutterOptionPane.getSelectionAreaWidth
         val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
         val FOLD_MARKER_SIZE = 12
 
         if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
-          Isabelle.swing_buffer_lock(model.buffer) {
+          Isabelle.buffer_lock(model.buffer) {
             val snapshot = update_snapshot()
             for (i <- 0 until physical_lines.length) {
               if (physical_lines(i) != -1) {
@@ -365,32 +369,36 @@
       react {
         case changed: Session.Commands_Changed =>
           val buffer = model.buffer
-          Isabelle.swing_buffer_lock(buffer) {
-            val (updated, snapshot) = flush_snapshot()
+          Swing_Thread.later {
+            Isabelle.buffer_lock(buffer) {
+              if (model.buffer == text_area.getBuffer) {
+                val (updated, snapshot) = flush_snapshot()
 
-            if (updated ||
-                (changed.nodes.contains(model.name) &&
-                 changed.commands.exists(snapshot.node.commands.contains)))
-              overview.delay_repaint(true)
+                if (updated ||
+                    (changed.nodes.contains(model.name) &&
+                     changed.commands.exists(snapshot.node.commands.contains)))
+                  overview.delay_repaint(true)
 
-            visible_range() match {
-              case None =>
-              case Some(visible) =>
-                if (updated) invalidate_range(visible)
-                else {
-                  val visible_cmds =
-                    snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
-                  if (visible_cmds.exists(changed.commands)) {
-                    for {
-                      line <- 0 until text_area.getVisibleLines
-                      val start = text_area.getScreenLineStartOffset(line) if start >= 0
-                      val end = text_area.getScreenLineEndOffset(line) if end >= 0
-                      val range = proper_line_range(start, end)
-                      val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
-                      if line_cmds.exists(changed.commands)
-                    } text_area.invalidateScreenLineRange(line, line)
-                  }
+                visible_range() match {
+                  case Some(visible) =>
+                    if (updated) invalidate_range(visible)
+                    else {
+                      val visible_cmds =
+                        snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
+                      if (visible_cmds.exists(changed.commands)) {
+                        for {
+                          line <- 0 until text_area.getVisibleLines
+                          val start = text_area.getScreenLineStartOffset(line) if start >= 0
+                          val end = text_area.getScreenLineEndOffset(line) if end >= 0
+                          val range = proper_line_range(start, end)
+                          val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
+                          if line_cmds.exists(changed.commands)
+                        } text_area.invalidateScreenLineRange(line, line)
+                      }
+                    }
+                  case None =>
                 }
+              }
             }
           }
 
diff -r 571ce2bc0b64 -r efb98d27dc1a src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Mar 14 22:34:18 2012 +0100
@@ -81,8 +81,10 @@
 
   override def complete(pane: EditPane, caret: Text.Offset): SideKickCompletion =
   {
+    Swing_Thread.assert()
+
     val buffer = pane.getBuffer
-    Isabelle.swing_buffer_lock(buffer) {
+    Isabelle.buffer_lock(buffer) {
       Document_Model(buffer) match {
         case None => null
         case Some(model) =>
diff -r 571ce2bc0b64 -r efb98d27dc1a src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Mar 14 22:34:18 2012 +0100
@@ -386,7 +386,7 @@
         case phase: Session.Phase =>
           phase match {
             case Session.Failed =>
-              Swing_Thread.now {
+              Swing_Thread.later {
                 val text = new scala.swing.TextArea(Isabelle.session.current_syslog())
                 text.editable = false
                 Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
@@ -445,7 +445,7 @@
         }
 
       case msg: PropertiesChanged =>
-        Swing_Thread.now { Isabelle.setup_tooltips() }
+        Isabelle.setup_tooltips()
         Isabelle.session.global_settings.event(Session.Global_Settings)
 
       case _ =>
diff -r 571ce2bc0b64 -r efb98d27dc1a src/Tools/jEdit/src/protocol_dockable.scala
--- a/src/Tools/jEdit/src/protocol_dockable.scala	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Tools/jEdit/src/protocol_dockable.scala	Wed Mar 14 22:34:18 2012 +0100
@@ -29,10 +29,10 @@
     loop {
       react {
         case input: Isabelle_Process.Input =>
-          Swing_Thread.now { text_area.append(input.toString + "\n") }
+          Swing_Thread.later { text_area.append(input.toString + "\n") }
 
         case output: Isabelle_Process.Output =>
-          Swing_Thread.now { text_area.append(output.message.toString + "\n") }
+          Swing_Thread.later { text_area.append(output.message.toString + "\n") }
 
         case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
       }
diff -r 571ce2bc0b64 -r efb98d27dc1a src/Tools/jEdit/src/raw_output_dockable.scala
--- a/src/Tools/jEdit/src/raw_output_dockable.scala	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Wed Mar 14 22:34:18 2012 +0100
@@ -31,7 +31,7 @@
       react {
         case output: Isabelle_Process.Output =>
           if (output.is_stdout || output.is_stderr)
-            Swing_Thread.now { text_area.append(XML.content(output.message).mkString) }
+            Swing_Thread.later { text_area.append(XML.content(output.message).mkString) }
 
         case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
       }
diff -r 571ce2bc0b64 -r efb98d27dc1a src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Tools/jEdit/src/session_dockable.scala	Wed Mar 14 22:34:18 2012 +0100
@@ -175,13 +175,13 @@
       react {
         case output: Isabelle_Process.Output =>
           if (output.is_syslog)
-            Swing_Thread.now {
+            Swing_Thread.later {
               val text = Isabelle.session.current_syslog()
               if (text != syslog.text) syslog.text = text
             }
 
         case phase: Session.Phase =>
-          Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
+          Swing_Thread.later { session_phase.text = " " + phase.toString + " " }
 
         case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))