# HG changeset patch
# User wenzelm
# Date 1332449006 -3600
# Node ID eba1cea4eef6c39bf104afa8adfac5f05ee98300
# Parent  08c22e8ffe70d0a6a9f040dcc62ecb23d2f67b18# Parent  737d7bc8e50fe9b17d9cd2ef77049489ecaba306
merged;

diff -r 08c22e8ffe70 -r eba1cea4eef6 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Thu Mar 22 18:54:39 2012 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Thu Mar 22 21:43:26 2012 +0100
@@ -14,7 +14,7 @@
 text {*
 
 For more lemmas about the extended real numbers go to
-  @{text "src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"}
+  @{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"}
 
 *}
 
@@ -127,7 +127,7 @@
 instantiation ereal :: number
 begin
 definition [simp]: "number_of x = ereal (number_of x)"
-instance proof qed
+instance ..
 end
 
 instantiation ereal :: abs
@@ -184,11 +184,12 @@
 
 instance
 proof
-  fix a :: ereal show "0 + a = a"
+  fix a b c :: ereal
+  show "0 + a = a"
     by (cases a) (simp_all add: zero_ereal_def)
-  fix b :: ereal show "a + b = b + a"
+  show "a + b = b + a"
     by (cases rule: ereal2_cases[of a b]) simp_all
-  fix c :: ereal show "a + b + c = a + (b + c)"
+  show "a + b + c = a + (b + c)"
     by (cases rule: ereal3_cases[of a b c]) simp_all
 qed
 end
@@ -232,7 +233,8 @@
 
 lemma real_of_ereal_add:
   fixes a b :: ereal
-  shows "real (a + b) = (if (\<bar>a\<bar> = \<infinity>) \<and> (\<bar>b\<bar> = \<infinity>) \<or> (\<bar>a\<bar> \<noteq> \<infinity>) \<and> (\<bar>b\<bar> \<noteq> \<infinity>) then real a + real b else 0)"
+  shows "real (a + b) =
+    (if (\<bar>a\<bar> = \<infinity>) \<and> (\<bar>b\<bar> = \<infinity>) \<or> (\<bar>a\<bar> \<noteq> \<infinity>) \<and> (\<bar>b\<bar> \<noteq> \<infinity>) then real a + real b else 0)"
   by (cases rule: ereal2_cases[of a b]) auto
 
 subsubsection "Linear order on @{typ ereal}"
@@ -240,13 +242,14 @@
 instantiation ereal :: linorder
 begin
 
-function less_ereal where
-"   ereal x < ereal y     \<longleftrightarrow> x < y" |
-"(\<infinity>::ereal) < a           \<longleftrightarrow> False" |
-"         a < -(\<infinity>::ereal) \<longleftrightarrow> False" |
-"ereal x    < \<infinity>           \<longleftrightarrow> True" |
-"        -\<infinity> < ereal r     \<longleftrightarrow> True" |
-"        -\<infinity> < (\<infinity>::ereal) \<longleftrightarrow> True"
+function less_ereal
+where
+  "   ereal x < ereal y     \<longleftrightarrow> x < y"
+| "(\<infinity>::ereal) < a           \<longleftrightarrow> False"
+| "         a < -(\<infinity>::ereal) \<longleftrightarrow> False"
+| "ereal x    < \<infinity>           \<longleftrightarrow> True"
+| "        -\<infinity> < ereal r     \<longleftrightarrow> True"
+| "        -\<infinity> < (\<infinity>::ereal) \<longleftrightarrow> True"
 proof -
   case (goal1 P x)
   moreover then obtain a b where "x = (a,b)" by (cases x) auto
@@ -290,17 +293,19 @@
 
 instance
 proof
-  fix x :: ereal show "x \<le> x"
+  fix x y z :: ereal
+  show "x \<le> x"
     by (cases x) simp_all
-  fix y :: ereal show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
+  show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
     by (cases rule: ereal2_cases[of x y]) auto
   show "x \<le> y \<or> y \<le> x "
     by (cases rule: ereal2_cases[of x y]) auto
   { assume "x \<le> y" "y \<le> x" then show "x = y"
     by (cases rule: ereal2_cases[of x y]) auto }
-  { fix z assume "x \<le> y" "y \<le> z" then show "x \<le> z"
+  { assume "x \<le> y" "y \<le> z" then show "x \<le> z"
     by (cases rule: ereal3_cases[of x y z]) auto }
 qed
+
 end
 
 instance ereal :: ordered_ab_semigroup_add
@@ -430,16 +435,20 @@
   fixes x :: ereal assumes "\<And>B. x \<le> ereal B" shows "x = - \<infinity>"
 proof (cases x)
   case (real r) with assms[of "r - 1"] show ?thesis by auto
-next case PInf with assms[of 0] show ?thesis by auto
-next case MInf then show ?thesis by simp
+next
+  case PInf with assms[of 0] show ?thesis by auto
+next
+  case MInf then show ?thesis by simp
 qed
 
 lemma ereal_top:
   fixes x :: ereal assumes "\<And>B. x \<ge> ereal B" shows "x = \<infinity>"
 proof (cases x)
   case (real r) with assms[of "r + 1"] show ?thesis by auto
-next case MInf with assms[of 0] show ?thesis by auto
-next case PInf then show ?thesis by simp
+next
+  case MInf with assms[of 0] show ?thesis by auto
+next
+  case PInf then show ?thesis by simp
 qed
 
 lemma
@@ -516,11 +525,11 @@
 
 instance
 proof
-  fix a :: ereal show "1 * a = a"
+  fix a b c :: ereal show "1 * a = a"
     by (cases a) (simp_all add: one_ereal_def)
-  fix b :: ereal show "a * b = b * a"
+  show "a * b = b * a"
     by (cases rule: ereal2_cases[of a b]) simp_all
-  fix c :: ereal show "a * b * c = a * (b * c)"
+  show "a * b * c = a * (b * c)"
     by (cases rule: ereal3_cases[of a b c])
        (simp_all add: zero_ereal_def zero_less_mult_iff)
 qed
@@ -668,11 +677,11 @@
   shows "x <= y"
 proof-
 { assume a: "EX r. y = ereal r"
-  from this obtain r where r_def: "y = ereal r" by auto
+  then obtain r where r_def: "y = ereal r" by auto
   { assume "x=(-\<infinity>)" hence ?thesis by auto }
   moreover
   { assume "~(x=(-\<infinity>))"
-    from this obtain p where p_def: "x = ereal p"
+    then obtain p where p_def: "x = ereal p"
     using a assms[rule_format, of 1] by (cases x) auto
     { fix e have "0 < e --> p <= r + e"
       using assms[rule_format, of "ereal e"] p_def r_def by auto }
@@ -696,10 +705,10 @@
   { assume "e=\<infinity>" hence "x<=y+e" by auto }
   moreover
   { assume "e~=\<infinity>"
-    from this obtain r where "e = ereal r" using `e>0` apply (cases e) by auto
+    then obtain r where "e = ereal r" using `e>0` apply (cases e) by auto
     hence "x<=y+e" using assms[rule_format, of r] `e>0` by auto
   } ultimately have "x<=y+e" by blast
-} from this show ?thesis using ereal_le_epsilon by auto
+} then show ?thesis using ereal_le_epsilon by auto
 qed
 
 lemma ereal_le_real:
@@ -790,11 +799,14 @@
 
 lemma ereal_uminus_lessThan[simp]:
   fixes a :: ereal shows "uminus ` {..<a} = {-a<..}"
-proof (safe intro!: image_eqI)
-  fix x assume "-a < x"
-  then have "- x < - (- a)" by (simp del: ereal_uminus_uminus)
-  then show "- x < a" by simp
-qed auto
+proof -
+  {
+    fix x assume "-a < x"
+    then have "- x < - (- a)" by (simp del: ereal_uminus_uminus)
+    then have "- x < a" by simp
+  }
+  then show ?thesis by (auto intro!: image_eqI)
+qed
 
 lemma ereal_uminus_greaterThan[simp]:
   "uminus ` {(a::ereal)<..} = {..<-a}"
@@ -923,7 +935,8 @@
   assumes "\<bar>x\<bar> \<noteq> \<infinity>" "0 < e"
   shows "x - e < x" "x < x + e"
 using assms apply (cases x, cases e) apply auto
-using assms by (cases x, cases e) auto
+using assms apply (cases x, cases e) apply auto
+done
 
 subsubsection {* Division *}
 
@@ -939,7 +952,7 @@
 
 definition "x / y = x * inverse (y :: ereal)"
 
-instance proof qed
+instance ..
 end
 
 lemma real_of_ereal_inverse[simp]:
@@ -1092,7 +1105,7 @@
 begin
 definition [simp]: "sup x y = (max x y :: ereal)"
 definition [simp]: "inf x y = (min x y :: ereal)"
-instance proof qed simp_all
+instance by default simp_all
 end
 
 instantiation ereal :: complete_lattice
@@ -1161,7 +1174,7 @@
 proof-
 def S1 == "uminus ` S"
 hence "S1 ~= {}" using assms by auto
-from this obtain x where x_def: "(ALL y:S1. y <= x) & (ALL z. (ALL y:S1. y <= z) --> x <= z)"
+then obtain x where x_def: "(ALL y:S1. y <= x) & (ALL z. (ALL y:S1. y <= z) --> x <= z)"
    using ereal_complete_Sup[of S1] by auto
 { fix z assume "ALL y:S. z <= y"
   hence "ALL y:S1. y <= -z" unfolding S1_def by auto
@@ -1372,8 +1385,8 @@
 proof-
 { assume "?rhs"
   { assume "~(x <= (SUP i:A. f i))" hence "(SUP i:A. f i)<x" by (simp add: not_le)
-    from this obtain y where y_def: "(SUP i:A. f i)<y & y<x" using ereal_dense by auto
-    from this obtain i where "i : A & y <= f i" using `?rhs` by auto
+    then obtain y where y_def: "(SUP i:A. f i)<y & y<x" using ereal_dense by auto
+    then obtain i where "i : A & y <= f i" using `?rhs` by auto
     hence "y <= (SUP i:A. f i)" using SUP_upper[of i A f] by auto
     hence False using y_def by auto
   } hence "?lhs" by auto
@@ -1391,8 +1404,8 @@
 proof-
 { assume "?rhs"
   { assume "~((INF i:A. f i) <= x)" hence "x < (INF i:A. f i)" by (simp add: not_le)
-    from this obtain y where y_def: "x<y & y<(INF i:A. f i)" using ereal_dense by auto
-    from this obtain i where "i : A & f i <= y" using `?rhs` by auto
+    then obtain y where y_def: "x<y & y<(INF i:A. f i)" using ereal_dense by auto
+    then obtain i where "i : A & f i <= y" using `?rhs` by auto
     hence "(INF i:A. f i) <= y" using INF_lower[of i A f] by auto
     hence False using y_def by auto
   } hence "?lhs" by auto
@@ -2023,7 +2036,7 @@
   shows "Y ----> L"
 proof-
 { fix S assume "open S" and "L:S"
-  from this obtain N1 where "ALL n>=N1. X n : S"
+  then obtain N1 where "ALL n>=N1. X n : S"
      using assms unfolding tendsto_def eventually_sequentially by auto
   hence "ALL n>=max N N1. Y n : S" using assms by auto
   hence "EX N. ALL n>=N. Y n : S" apply(rule_tac x="max N N1" in exI) by auto
@@ -2058,14 +2071,14 @@
     hence ?thesis by auto }
   moreover
   { assume "EX B. C = ereal B"
-    from this obtain B where B_def: "C=ereal B" by auto
+    then obtain B where B_def: "C=ereal B" by auto
     hence "~(l=\<infinity>)" using Lim_bounded_PInfty2 assms by auto
-    from this obtain m where m_def: "ereal m=l" using `~(l=(-\<infinity>))` by (cases l) auto
-    from this obtain N where N_def: "ALL n>=N. f n : {ereal(m - 1) <..< ereal(m+1)}"
+    then obtain m where m_def: "ereal m=l" using `~(l=(-\<infinity>))` by (cases l) auto
+    then obtain N where N_def: "ALL n>=N. f n : {ereal(m - 1) <..< ereal(m+1)}"
        apply (subst tendsto_obtains_N[of f l "{ereal(m - 1) <..< ereal(m+1)}"]) using assms by auto
     { fix n assume "n>=N"
       hence "EX r. ereal r = f n" using N_def by (cases "f n") auto
-    } from this obtain g where g_def: "ALL n>=N. ereal (g n) = f n" by metis
+    } then obtain g where g_def: "ALL n>=N. ereal (g n) = f n" by metis
     hence "(%n. ereal (g n)) ----> l" using tail_same_limit[of f l N] assms by auto
     hence *: "(%n. g n) ----> m" using m_def by auto
     { fix n assume "n>=max N M"
@@ -2175,7 +2188,7 @@
     fix N assume "n <= N"
     from upper[OF this] lower[OF this] assms `0 < r`
     have "u N ~: {\<infinity>,(-\<infinity>)}" by auto
-    from this obtain ra where ra_def: "(u N) = ereal ra" by (cases "u N") auto
+    then obtain ra where ra_def: "(u N) = ereal ra" by (cases "u N") auto
     hence "rx < ra + r" and "ra < rx + r"
        using rx_def assms `0 < r` lower[OF `n <= N`] upper[OF `n <= N`] by auto
     hence "dist (real (u N)) rx < r"
@@ -2194,7 +2207,7 @@
 proof
   assume lim: "u ----> x"
   { fix r assume "(r::ereal)>0"
-    from this obtain N where N_def: "ALL n>=N. u n : {x - r <..< x + r}"
+    then obtain N where N_def: "ALL n>=N. u n : {x - r <..< x + r}"
        apply (subst tendsto_obtains_N[of u x "{x - r <..< x + r}"])
        using lim ereal_between[of x r] assms `r>0` by auto
     hence "EX N. ALL n>=N. u n < x + r & x < u n + r"
@@ -2537,8 +2550,8 @@
 
 lemma real_ereal_id: "real o ereal = id"
 proof-
-{ fix x have "(real o ereal) x = id x" by auto }
-from this show ?thesis using ext by blast
+  { fix x have "(real o ereal) x = id x" by auto }
+  then show ?thesis using ext by blast
 qed
 
 lemma open_image_ereal: "open(UNIV-{ \<infinity> , (-\<infinity> :: ereal)})"
diff -r 08c22e8ffe70 -r eba1cea4eef6 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Mar 22 18:54:39 2012 +0100
+++ b/src/Pure/Isar/class.ML	Thu Mar 22 21:43:26 2012 +0100
@@ -145,10 +145,12 @@
 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);
+
 val export_morphism = #export_morph oo the_class_data;
 
 fun print_classes ctxt =
@@ -228,9 +230,9 @@
     val intros = (snd o rules thy) sup :: map_filter I
       [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_wit,
         (fst o rules thy) sub];
-    val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
-    val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
-      (K tac);
+    val classrel =
+      Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
+        (K (EVERY (map (TRYALL o Tactic.rtac) intros)));
     val diff_sort = Sign.complete_sort thy [sup]
       |> subtract (op =) (Sign.complete_sort thy [sub])
       |> filter (is_class thy);
@@ -312,13 +314,13 @@
 
 val class_prefix = Logic.const_of_class o Long_Name.base_name;
 
+local
+
 fun target_extension f class lthy =
   lthy
   |> Local_Theory.raw_theory f
-  |> Local_Theory.target (synchronize_class_syntax [class]
-      (base_sort (Proof_Context.theory_of lthy) class));
-
-local
+  |> Local_Theory.map_contexts
+      (synchronize_class_syntax [class] (base_sort (Proof_Context.theory_of lthy) class));
 
 fun target_const class ((c, mx), (type_params, dict)) thy =
   let
@@ -478,10 +480,11 @@
 
 (* target *)
 
-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))
+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;
+  ##> Local_Theory.map_contexts synchronize_inst_syntax;
 
 fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   (case instantiation_param lthy b of
@@ -554,7 +557,7 @@
         abbrev = Generic_Target.abbrev
           (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
             Generic_Target.theory_abbrev prmode ((b, mx), t)),
-        declaration = K Generic_Target.theory_declaration,
+        declaration = K Generic_Target.standard_declaration,
         pretty = pretty,
         exit = Local_Theory.target_of o conclude}
   end;
@@ -603,8 +606,8 @@
     val (tycos, vs, sort) = read_multi_arity thy raw_arities;
     val sorts = map snd vs;
     val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
-    fun after_qed results = Proof_Context.background_theory
-      ((fold o fold) AxClass.add_arity results);
+    fun after_qed results =
+      Proof_Context.background_theory ((fold o fold) AxClass.add_arity results);
   in
     thy
     |> Proof_Context.init_global
diff -r 08c22e8ffe70 -r eba1cea4eef6 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Thu Mar 22 18:54:39 2012 +0100
+++ b/src/Pure/Isar/generic_target.ML	Thu Mar 22 21:43:26 2012 +0100
@@ -20,7 +20,9 @@
     string * bool -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
 
-  val theory_declaration: declaration -> local_theory -> local_theory
+  val background_declaration: declaration -> local_theory -> local_theory
+  val standard_declaration: declaration -> local_theory -> local_theory
+
   val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
     term list * term list -> local_theory -> (term * thm) * local_theory
   val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list ->
@@ -88,8 +90,7 @@
 
     (*note*)
     val ([(res_name, [res])], lthy4) = lthy3
-      |> Local_Theory.notes_kind ""
-        [((if internal then Binding.empty else b_def, atts), [([def], [])])];
+      |> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])];
   in ((lhs, (res_name, res)), lthy4) end;
 
 
@@ -180,20 +181,24 @@
   end;
 
 
+(* declaration *)
+
+fun background_declaration decl lthy =
+  let
+    val theory_decl =
+      Local_Theory.standard_form lthy
+        (Proof_Context.init_global (Proof_Context.theory_of lthy)) decl;
+  in Local_Theory.background_theory (Context.theory_map theory_decl) lthy end;
+
+fun standard_declaration decl =
+  background_declaration decl #>
+  (fn lthy => Local_Theory.map_contexts (fn ctxt =>
+    Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt) lthy);
+
+
 
 (** primitive theory operations **)
 
-fun theory_declaration decl lthy =
-  let
-    val global_decl = Morphism.form
-      (Morphism.transform (Local_Theory.global_morphism lthy) decl);
-  in
-    lthy
-    |> Local_Theory.background_theory (Context.theory_map global_decl)
-    |> Local_Theory.target (Context.proof_map global_decl)
-    |> Context.proof_map (Morphism.form decl)
-  end;
-
 fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   let
     val (const, lthy2) = lthy
diff -r 08c22e8ffe70 -r eba1cea4eef6 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Thu Mar 22 18:54:39 2012 +0100
+++ b/src/Pure/Isar/local_theory.ML	Thu Mar 22 21:43:26 2012 +0100
@@ -33,7 +33,7 @@
   val propagate_ml_env: generic_theory -> generic_theory
   val standard_morphism: local_theory -> Proof.context -> morphism
   val target_morphism: local_theory -> morphism
-  val global_morphism: local_theory -> morphism
+  val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
   val operations_of: local_theory -> operations
   val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
@@ -99,7 +99,12 @@
 );
 
 fun map_contexts f =
-  (Data.map o map) (fn {naming, operations, target} => make_lthy (naming, operations, f target))
+  (Data.map o map) (fn {naming, operations, target} =>
+    make_lthy (naming, operations,
+      target
+      |> Context_Position.set_visible false
+      |> f
+      |> Context_Position.restore_visible target))
   #> f;
 
 fun assert lthy =
@@ -178,10 +183,11 @@
 
 fun target_result f lthy =
   let
-    val (res, ctxt') = target_of lthy
+    val target = target_of lthy;
+    val (res, ctxt') = target
       |> Context_Position.set_visible false
       |> f
-      ||> Context_Position.restore_visible lthy;
+      ||> Context_Position.restore_visible target;
     val thy' = Proof_Context.theory_of ctxt';
     val lthy' = lthy
       |> map_target (K ctxt')
@@ -208,8 +214,8 @@
 
 fun target_morphism lthy = standard_morphism lthy (target_of lthy);
 
-fun global_morphism lthy =
-  standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
+fun standard_form lthy ctxt x =
+  Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
 
 
 
diff -r 08c22e8ffe70 -r eba1cea4eef6 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Thu Mar 22 18:54:39 2012 +0100
+++ b/src/Pure/Isar/named_target.ML	Thu Mar 22 21:43:26 2012 +0100
@@ -61,12 +61,10 @@
   end;
 
 fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy =
-  if target = "" then Generic_Target.theory_declaration decl lthy
+  if target = "" then Generic_Target.standard_declaration decl lthy
   else
     lthy
-    |> pervasive ? Local_Theory.background_theory
-        (Context.theory_map
-          (Morphism.form (Morphism.transform (Local_Theory.global_morphism lthy) decl)))
+    |> pervasive ? Generic_Target.background_declaration decl
     |> locale_declaration target syntax decl
     |> Context.proof_map (Morphism.form decl);
 
@@ -133,7 +131,7 @@
     lthy
     |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
     |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
-  end
+  end;
 
 fun target_notes (Target {target, is_locale, ...}) =
   if is_locale then locale_notes target
diff -r 08c22e8ffe70 -r eba1cea4eef6 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Thu Mar 22 18:54:39 2012 +0100
+++ b/src/Pure/Isar/overloading.ML	Thu Mar 22 21:43:26 2012 +0100
@@ -155,7 +155,7 @@
       (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
+  ##> Local_Theory.map_contexts synchronize_syntax
   #-> (fn (_, def) => pair (Const (c, U), def));
 
 fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
@@ -208,7 +208,7 @@
         abbrev = Generic_Target.abbrev
           (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
             Generic_Target.theory_abbrev prmode ((b, mx), t)),
-        declaration = K Generic_Target.theory_declaration,
+        declaration = K Generic_Target.standard_declaration,
         pretty = pretty,
         exit = Local_Theory.target_of o conclude}
   end;
diff -r 08c22e8ffe70 -r eba1cea4eef6 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Mar 22 18:54:39 2012 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Mar 22 21:43:26 2012 +0100
@@ -220,8 +220,7 @@
     val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);
 
     val ([(def_name, [th'])], lthy4) = lthy3
-      |> Local_Theory.notes_kind ""
-        [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])];
+      |> Local_Theory.notes [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])];
 
     val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;