# HG changeset patch
# User krauss
# Date 1333315314 -7200
# Node ID 4c7548e7df86d574c8fc915c0929556c4c1a28f3
# Parent  bf9796e445846c1899e6cdef93ca3637d8f28ea4# Parent  434d9dd99523022ce0e40c5086eac78e424c25ea
merged, manually resolving conflicts due to session renaming (cf. 6488c5efec49)

diff -r bf9796e44584 -r 4c7548e7df86 Admin/update-keywords
--- a/Admin/update-keywords	Sun Apr 01 23:09:36 2012 +0200
+++ b/Admin/update-keywords	Sun Apr 01 23:21:54 2012 +0200
@@ -13,7 +13,7 @@
 isabelle keywords \
   "$LOG/Pure.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/HOL-Boogie.gz" \
   "$LOG/HOL-Library.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz" \
-  "$LOG/HOL-SPARK.gz" "$LOG/HOL-TPTP.gz"
+  "$LOG/HOL-SPARK.gz" "$LOG/HOL-TPTP.gz" "$LOG/HOL-Import.gz"
 
 isabelle keywords -k ZF \
   "$LOG/Pure.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
diff -r bf9796e44584 -r 4c7548e7df86 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Sun Apr 01 23:09:36 2012 +0200
+++ b/etc/isar-keywords.el	Sun Apr 01 23:21:54 2012 +0200
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP.
+;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP + HOL-Import.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
@@ -108,7 +108,10 @@
     "hide_const"
     "hide_fact"
     "hide_type"
+    "import_const_map"
+    "import_file"
     "import_tptp"
+    "import_type_map"
     "include"
     "including"
     "inductive"
@@ -491,7 +494,10 @@
     "hide_const"
     "hide_fact"
     "hide_type"
+    "import_const_map"
+    "import_file"
     "import_tptp"
+    "import_type_map"
     "inductive"
     "inductive_set"
     "instantiation"
diff -r bf9796e44584 -r 4c7548e7df86 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Sun Apr 01 23:09:36 2012 +0200
+++ b/lib/scripts/getsettings	Sun Apr 01 23:21:54 2012 +0200
@@ -92,7 +92,7 @@
 #robust invocation via ISABELLE_JDK_HOME
 function isabelle_jdk () {
   [ -z "$ISABELLE_JDK_HOME" ] && \
-    { echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable"; exit 2; }
+    { echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2; return 2; }
   local PRG="$1"; shift
   "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
 }
@@ -100,7 +100,7 @@
 #robust invocation via SCALA_HOME
 function isabelle_scala () {
   [ -z "$SCALA_HOME" ] && \
-    { echo "Unknown SCALA_HOME -- Scala unavailable"; exit 2; }
+    { echo "Unknown SCALA_HOME -- Scala unavailable" >&2; return 2; }
   local PRG="$1"; shift
   "$SCALA_HOME/bin/$PRG" "$@"
 }
diff -r bf9796e44584 -r 4c7548e7df86 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sun Apr 01 23:09:36 2012 +0200
+++ b/src/HOL/IsaMakefile	Sun Apr 01 23:21:54 2012 +0200
@@ -548,7 +548,7 @@
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IMPP
 
 
-## Import sessions
+## HOL-Import
 
 HOL-Import: $(LOG)/HOL-Import.gz
 
@@ -561,6 +561,7 @@
   Import/HOL_Light_Import.thy
 	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Import
 
+
 ## HOL-Number_Theory
 
 HOL-Number_Theory: HOL $(LOG)/HOL-Number_Theory.gz
@@ -1785,9 +1786,10 @@
 	@rm -f $(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz			\
 		$(LOG)/HOL-Bali.gz $(LOG)/HOL-Base.gz			\
 		$(LOG)/HOL-Boogie-Examples.gz $(LOG)/HOL-Boogie.gz	\
-		$(LOG)/HOL-Decision_Procs.gz $(LOG)/HOL-Hahn_Banach.gz	\
-		$(LOG)/HOL-Hoare.gz $(LOG)/HOL-Hoare_Parallel.gz	\
-		$(LOG)/HOL-IMP.gz $(LOG)/HOL-IMPP.gz $(LOG)/HOL-IOA.gz	\
+		$(LOG)/HOL-Decision_Procs.gz $(LOG)/HOL-HOL_Light.gz	\
+		$(LOG)/HOL-Hahn_Banach.gz $(LOG)/HOL-Hoare.gz		\
+		$(LOG)/HOL-Hoare_Parallel.gz $(LOG)/HOL-IMP.gz		\
+		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-IOA.gz			\
 		$(LOG)/HOL-Imperative_HOL.gz $(LOG)/HOL-Import.gz	\
 		$(LOG)/HOL-Induct.gz $(LOG)/HOL-Isar_Examples.gz	\
 		$(LOG)/HOL-Lattice $(LOG)/HOL-Lattice.gz		\
@@ -1817,18 +1819,17 @@
 		$(LOG)/HOL-TPTP.gz $(LOG)/HOL-UNITY.gz			\
 		$(LOG)/HOL-Unix.gz $(LOG)/HOL-Word-Examples.gz		\
 		$(LOG)/HOL-Word.gz $(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz	\
-		$(LOG)/HOL.gz $(LOG)/TLA-Buffer.gz			\
-		$(LOG)/TLA-Inc.gz $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz	\
-		$(OUT)/HOL $(OUT)/HOL-Algebra $(OUT)/HOL-Base		\
-		$(OUT)/HOL-Boogie $(OUT)/HOL-IMP $(OUT)/HOL-Library	\
+		$(LOG)/HOL.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz	\
+		$(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL		\
+		$(OUT)/HOL-Algebra $(OUT)/HOL-Base $(OUT)/HOL-Boogie	\
+		$(OUT)/HOL-HOL_Light $(OUT)/HOL-IMP $(OUT)/HOL-Library	\
 		$(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis	\
 		$(OUT)/HOL-NSA $(OUT)/HOL-Nominal $(OUT)/HOL-Plain	\
 		$(OUT)/HOL-Probability $(OUT)/HOL-Proofs		\
-		$(OUT)/HOL-SPARK $(OUT)/HOL-Word			\
-		$(OUT)/TLA $(OUT)/HOLCF $(LOG)/HOLCF.gz			\
-		$(LOG)/HOLCF-IMP.gz $(LOG)/HOLCF-ex.gz			\
-		$(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA $(LOG)/IOA.gz		\
-		$(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz			\
+		$(OUT)/HOL-SPARK $(OUT)/HOL-Word $(OUT)/TLA		\
+		$(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz	\
+		$(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA	\
+		$(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz	\
 		$(LOG)/IOA-Storage.gz $(LOG)/HOLCF-Library.gz		\
 		$(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz		\
 		$(LOG)/HOL-Datatype_Benchmark.gz			\
diff -r bf9796e44584 -r 4c7548e7df86 src/HOL/Library/Fraction_Field.thy
--- a/src/HOL/Library/Fraction_Field.thy	Sun Apr 01 23:09:36 2012 +0200
+++ b/src/HOL/Library/Fraction_Field.thy	Sun Apr 01 23:21:54 2012 +0200
@@ -146,14 +146,15 @@
 qed
 
 lemma mult_fract_cancel:
-  assumes "c \<noteq> 0"
+  assumes "c \<noteq> (0::'a)"
   shows "Fract (c * a) (c * b) = Fract a b"
 proof -
   from assms have "Fract c c = Fract 1 1" by (simp add: Fract_def)
   then show ?thesis by (simp add: mult_fract [symmetric])
 qed
 
-instance proof
+instance
+proof
   fix q r s :: "'a fract" show "(q * r) * s = q * (r * s)" 
     by (cases q, cases r, cases s) (simp add: eq_fract algebra_simps)
 next
@@ -249,7 +250,8 @@
 lemma divide_fract [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
   by (simp add: divide_fract_def)
 
-instance proof
+instance
+proof
   fix q :: "'a fract"
   assume "q \<noteq> 0"
   then show "inverse q * q = 1"
@@ -328,7 +330,8 @@
   shows "Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)"
 by (simp add: less_fract_def less_le_not_le mult_ac assms)
 
-instance proof
+instance
+proof
   fix q r s :: "'a fract"
   assume "q \<le> r" and "r \<le> s" thus "q \<le> s"
   proof (induct q, induct r, induct s)
diff -r bf9796e44584 -r 4c7548e7df86 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Apr 01 23:09:36 2012 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Apr 01 23:21:54 2012 +0200
@@ -1420,14 +1420,12 @@
     val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds
       (maps_modes result_thms)
     val qname = #qname (dest_steps steps)
-    (* FIXME !? *)
-    val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute
-      (fn thm => Context.mapping (Code.add_eqn thm) I))))
+    val attrib = Thm.declaration_attribute (fn thm => Context.mapping (Code.add_eqn thm) I)
     val thy''' =
       cond_timeit (Config.get ctxt Quickcheck.timing) "Setting code equations...." (fn _ =>
       fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss
       [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
-        [attrib thy ])] thy))
+        [attrib])] thy))
       result_thms' thy'' |> Theory.checkpoint)
   in
     thy'''
diff -r bf9796e44584 -r 4c7548e7df86 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/attrib.ML	Sun Apr 01 23:21:54 2012 +0200
@@ -25,6 +25,12 @@
   val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) ->
     (('c * 'a list) * ('b * 'a list) list) list ->
     (('c * 'att list) * ('fact * 'att list) list) list
+  val global_notes: string -> (binding * (thm list * src list) list) list ->
+    theory -> (string * thm list) list * theory
+  val local_notes: string -> (binding * (thm list * src list) list) list ->
+    Proof.context -> (string * thm list) list * Proof.context
+  val generic_notes: string -> (binding * (thm list * src list) list) list ->
+    Context.generic -> (string * thm list) list * Context.generic
   val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
   val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
   val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
@@ -138,6 +144,15 @@
 
 (* fact expressions *)
 
+fun global_notes kind facts thy = thy |>
+  Global_Theory.note_thmss kind (map_facts (map (attribute_i thy)) facts);
+
+fun local_notes kind facts ctxt = ctxt |>
+  Proof_Context.note_thmss kind (map_facts (map (attribute_i (Proof_Context.theory_of ctxt))) facts);
+
+fun generic_notes kind facts context = context |>
+  Context.mapping_result (global_notes kind facts) (local_notes kind facts);
+
 fun eval_thms ctxt srcs = ctxt
   |> Proof_Context.note_thmss ""
     (map_facts_refs (map (attribute (Proof_Context.theory_of ctxt))) (Proof_Context.get_fact ctxt)
diff -r bf9796e44584 -r 4c7548e7df86 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/bundle.ML	Sun Apr 01 23:21:54 2012 +0200
@@ -15,12 +15,13 @@
     (binding * string option * mixfix) list -> local_theory -> local_theory
   val includes: string list -> Proof.context -> Proof.context
   val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context
-  val context_includes: string list -> generic_theory -> local_theory
-  val context_includes_cmd: (xstring * Position.T) list -> generic_theory -> local_theory
   val include_: string list -> Proof.state -> Proof.state
   val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
   val including: string list -> Proof.state -> Proof.state
   val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
+  val context: string list -> Element.context_i list -> generic_theory -> local_theory
+  val context_cmd: (xstring * Position.T) list -> Element.context list ->
+    generic_theory -> local_theory
   val print_bundles: Proof.context -> unit
 end;
 
@@ -87,29 +88,26 @@
 local
 
 fun gen_includes prep args ctxt =
-  let
-    val decls = maps (the_bundle ctxt o prep ctxt) args;
-    val attrib = Attrib.attribute_i (Proof_Context.theory_of ctxt);
-    val note = ((Binding.empty, []), map (apsnd (map attrib)) decls);
-  in #2 (Proof_Context.note_thmss "" [note] ctxt) end;
+  let val decls = maps (the_bundle ctxt o prep ctxt) args
+  in #2 (Attrib.local_notes "" [((Binding.empty, []), decls)] ctxt) end;
 
-fun gen_context prep args (Context.Theory thy) =
-      Named_Target.theory_init thy
-      |> Local_Theory.target (gen_includes prep args)
-      |> Local_Theory.restore
-  | gen_context prep args (Context.Proof lthy) =
-      Named_Target.assert lthy
-      |> gen_includes prep args
-      |> Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy);
+fun gen_context prep_bundle prep_stmt raw_incls raw_elems gthy =
+  let
+    val lthy = Context.cases Named_Target.theory_init Local_Theory.assert gthy;
+    val augment = gen_includes prep_bundle raw_incls #> prep_stmt raw_elems [] #> snd;
+  in
+    (case gthy of
+      Context.Theory _ => Local_Theory.target augment lthy |> Local_Theory.restore
+    | Context.Proof _ =>
+        augment lthy |>
+        Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy))
+  end;
 
 in
 
 val includes = gen_includes (K I);
 val includes_cmd = gen_includes check;
 
-val context_includes = gen_context (K I);
-val context_includes_cmd = gen_context check;
-
 fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts;
 fun include_cmd bs =
   Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.reset_facts;
@@ -117,6 +115,9 @@
 fun including bs = Proof.assert_backward #> Proof.map_context (includes bs);
 fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs);
 
+val context = gen_context (K I) Expression.cert_statement;
+val context_cmd = gen_context check Expression.read_statement;
+
 end;
 
 
diff -r bf9796e44584 -r 4c7548e7df86 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/class.ML	Sun Apr 01 23:21:54 2012 +0200
@@ -320,7 +320,7 @@
   lthy
   |> Local_Theory.raw_theory f
   |> Local_Theory.map_contexts
-      (synchronize_class_syntax [class] (base_sort (Proof_Context.theory_of lthy) class));
+      (K (synchronize_class_syntax [class] (base_sort (Proof_Context.theory_of lthy) class)));
 
 fun target_const class ((c, mx), (type_params, dict)) thy =
   let
@@ -484,7 +484,7 @@
   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.map_contexts synchronize_inst_syntax;
+  ##> Local_Theory.map_contexts (K synchronize_inst_syntax);
 
 fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   (case instantiation_param lthy b of
@@ -552,8 +552,7 @@
     |> synchronize_inst_syntax
     |> Local_Theory.init naming
        {define = Generic_Target.define foundation,
-        notes = Generic_Target.notes
-          (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
+        notes = Generic_Target.notes Generic_Target.theory_notes,
         abbrev = Generic_Target.abbrev
           (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
             Generic_Target.theory_abbrev prmode ((b, mx), t)),
diff -r bf9796e44584 -r 4c7548e7df86 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/element.ML	Sun Apr 01 23:21:54 2012 +0200
@@ -51,8 +51,6 @@
   val satisfy_morphism: witness list -> morphism
   val eq_morphism: theory -> thm list -> morphism option
   val transfer_morphism: theory -> morphism
-  val generic_note_thmss: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
-    Context.generic -> (string * thm list) list * Context.generic
   val init: context_i -> Context.generic -> Context.generic
   val activate_i: context_i -> Proof.context -> context_i * Proof.context
   val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
@@ -483,16 +481,6 @@
 
 (* init *)
 
-fun generic_note_thmss kind facts context =
-  let
-    val facts' =
-      Attrib.map_facts (map (Attrib.attribute_i (Context.theory_of context))) facts;
-  in
-    context |> Context.mapping_result
-      (Global_Theory.note_thmss kind facts')
-      (Proof_Context.note_thmss kind facts')
-  end;
-
 fun init (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
   | init (Constrains _) = I
   | init (Assumes asms) = Context.map_proof (fn ctxt =>
@@ -514,7 +502,7 @@
           |> fold Variable.auto_fixes (map #1 asms)
           |> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
       in ctxt' end)
-  | init (Notes (kind, facts)) = generic_note_thmss kind facts #> #2;
+  | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
 
 
 (* activate *)
diff -r bf9796e44584 -r 4c7548e7df86 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/expression.ML	Sun Apr 01 23:21:54 2012 +0200
@@ -816,7 +816,7 @@
 local
 
 fun note_eqns_register deps witss attrss eqns export export' =
-  Element.generic_note_thmss Thm.lemmaK
+  Attrib.generic_notes Thm.lemmaK
     (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
   #-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts)))
   #-> (fn eqns => fold (fn ((dep, morph), wits) =>
@@ -885,12 +885,10 @@
 
 fun note_eqns_dependency target deps witss attrss eqns export export' ctxt =
   let
-    val thy = Proof_Context.theory_of ctxt;
-
     val facts =
       (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
     val eqns' = ctxt
-      |> Proof_Context.note_thmss Thm.lemmaK (Attrib.map_facts (map (Attrib.attribute_i thy)) facts)
+      |> Attrib.local_notes Thm.lemmaK facts
       |-> (fn facts => `(fn ctxt => meta_rewrite ctxt (maps snd facts)))
       |> fst;  (* FIXME duplication to add_thmss *)
   in
diff -r bf9796e44584 -r 4c7548e7df86 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML	Sun Apr 01 23:21:54 2012 +0200
@@ -11,21 +11,26 @@
       term list * term list -> local_theory -> (term * thm) * local_theory) ->
     bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
-  val notes: (string -> (Attrib.binding * (thm list * Args.src list) list) list ->
+  val notes:
+    (string -> (Attrib.binding * (thm list * Args.src list) list) list ->
       (Attrib.binding * (thm list * Args.src list) list) list -> local_theory -> local_theory) ->
     string -> (Attrib.binding * (thm list * Args.src list) list) list -> local_theory ->
     (string * thm list) list * local_theory
+  val locale_notes: string -> string ->
+    (Attrib.binding * (thm list * Args.src list) list) list ->
+    (Attrib.binding * (thm list * Args.src list) list) list ->
+    local_theory -> local_theory
   val abbrev: (string * bool -> binding * mixfix -> term * term ->
       term list -> local_theory -> local_theory) ->
-    string * bool -> (binding * mixfix) * term -> local_theory ->
-    (term * term) * local_theory
-
+    string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
   val background_declaration: declaration -> local_theory -> local_theory
   val standard_declaration: declaration -> local_theory -> local_theory
-
+  val locale_declaration: string -> bool -> 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 ->
+  val theory_notes: string ->
+    (Attrib.binding * (thm list * Args.src list) list) list ->
+    (Attrib.binding * (thm list * Args.src list) list) list ->
     local_theory -> local_theory
   val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory
 end
@@ -95,6 +100,8 @@
 
 (* notes *)
 
+local
+
 fun import_export_proof ctxt (name, raw_th) =
   let
     val thy = Proof_Context.theory_of ctxt;
@@ -139,9 +146,13 @@
 
   in (result'', result) end;
 
+fun standard_facts lthy ctxt =
+  Element.transform_facts (Local_Theory.standard_morphism lthy ctxt);
+
+in
+
 fun notes target_notes kind facts lthy =
   let
-    val thy = Proof_Context.theory_of lthy;
     val facts' = facts
       |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
           (Local_Theory.full_name lthy (fst a))) bs))
@@ -150,10 +161,23 @@
     val global_facts = Global_Theory.map_facts #2 facts';
   in
     lthy
-    |> target_notes kind global_facts local_facts
-    |> Proof_Context.note_thmss kind (Attrib.map_facts (map (Attrib.attribute_i thy)) local_facts)
+    |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)
+    |> Attrib.local_notes kind local_facts
   end;
 
+fun locale_notes locale kind global_facts local_facts =
+  Local_Theory.background_theory
+    (Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #>
+  (fn lthy => lthy |>
+    Local_Theory.target (fn ctxt => ctxt |>
+      Locale.add_thmss locale kind (standard_facts lthy ctxt local_facts))) #>
+  (fn lthy => lthy |>
+    Local_Theory.map_contexts (fn level => fn ctxt =>
+      if level = 0 orelse level = Local_Theory.level lthy then ctxt
+      else ctxt |> Attrib.local_notes kind (standard_facts lthy ctxt local_facts) |> snd));
+
+end;
+
 
 (* abbrev *)
 
@@ -191,9 +215,14 @@
 
 fun standard_declaration decl =
   background_declaration decl #>
-  (fn lthy => Local_Theory.map_contexts (fn ctxt =>
+  (fn lthy => Local_Theory.map_contexts (fn _ => fn ctxt =>
     Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt) lthy);
 
+fun locale_declaration locale syntax decl lthy = lthy
+  |> Local_Theory.target (fn ctxt => ctxt |>
+    Locale.add_declaration locale syntax
+      (Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl));
+
 
 
 (** primitive theory operations **)
@@ -209,15 +238,13 @@
           (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
   in ((lhs, def), lthy3) end;
 
-fun theory_notes kind global_facts lthy =
-  let
-    val thy = Proof_Context.theory_of lthy;
-    val global_facts' = Attrib.map_facts (map (Attrib.attribute_i thy)) global_facts;
-  in
-    lthy
-    |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
-    |> Local_Theory.target (Proof_Context.note_thmss kind global_facts' #> snd)
-  end;
+fun theory_notes kind global_facts local_facts =
+  Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #>
+  (fn lthy => lthy |> Local_Theory.map_contexts (fn level => fn ctxt =>
+    if level = Local_Theory.level lthy then ctxt
+    else
+      ctxt |> Attrib.local_notes kind
+        (Element.transform_facts (Local_Theory.standard_morphism lthy ctxt) local_facts) |> snd));
 
 fun theory_abbrev prmode ((b, mx), t) =
   Local_Theory.background_theory
diff -r bf9796e44584 -r 4c7548e7df86 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sun Apr 01 23:21:54 2012 +0200
@@ -436,9 +436,10 @@
 
 val _ =
   Outer_Syntax.command ("context", Keyword.thy_decl) "begin local theory context"
-    ((Parse_Spec.includes >> (Toplevel.open_target o Bundle.context_includes_cmd) ||
-      Parse.position Parse.xname >> (fn name =>
-        Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)))
+    ((Parse.position Parse.xname >> (fn name =>
+        Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)) ||
+      Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
+        >> (fn (incls, elems) => Toplevel.open_target (Bundle.context_cmd incls elems)))
       --| Parse.begin);
 
 
diff -r bf9796e44584 -r 4c7548e7df86 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sun Apr 01 23:21:54 2012 +0200
@@ -10,12 +10,12 @@
 signature LOCAL_THEORY =
 sig
   type operations
-  val map_contexts: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val assert: local_theory -> local_theory
   val level: Proof.context -> int
   val assert_bottom: bool -> local_theory -> local_theory
   val open_target: Name_Space.naming -> operations -> local_theory -> local_theory
   val close_target: local_theory -> local_theory
+  val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
   val naming_of: local_theory -> Name_Space.naming
   val full_name: local_theory -> binding -> string
   val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
@@ -23,17 +23,16 @@
   val new_group: local_theory -> local_theory
   val reset_group: local_theory -> local_theory
   val restore_naming: local_theory -> local_theory -> local_theory
-  val target_of: local_theory -> Proof.context
+  val standard_morphism: local_theory -> Proof.context -> morphism
+  val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
   val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val raw_theory: (theory -> theory) -> local_theory -> local_theory
   val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val background_theory: (theory -> theory) -> local_theory -> local_theory
-  val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
+  val target_of: local_theory -> Proof.context
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
+  val target_morphism: local_theory -> morphism
   val propagate_ml_env: generic_theory -> generic_theory
-  val standard_morphism: local_theory -> Proof.context -> morphism
-  val target_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
@@ -98,21 +97,13 @@
   fun init _ = [];
 );
 
-fun map_contexts f =
-  (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 =
   if null (Data.get lthy) then error "Missing local theory context" else lthy;
 
-val get_lthy = hd o Data.get o assert;
+val get_last_lthy = List.last o Data.get o assert;
+val get_first_lthy = hd o Data.get o assert;
 
-fun map_lthy f = assert #>
+fun map_first_lthy f = assert #>
   Data.map (fn {naming, operations, target} :: parents =>
     make_lthy (f (naming, operations, target)) :: parents);
 
@@ -137,13 +128,25 @@
 fun close_target lthy =
   assert_bottom false lthy |> Data.map tl;
 
+fun map_contexts f lthy =
+  let val n = level lthy in
+    lthy |> (Data.map o map_index) (fn (i, {naming, operations, target}) =>
+      make_lthy (naming, operations,
+        target
+        |> Context_Position.set_visible false
+        |> f (n - i - 1)
+        |> Context_Position.restore_visible target))
+    |> f n
+  end;
+
 
 (* naming *)
 
-val naming_of = #naming o get_lthy;
+val naming_of = #naming o get_first_lthy;
 val full_name = Name_Space.full_name o naming_of;
 
-fun map_naming f = map_lthy (fn (naming, operations, target) => (f naming, operations, target));
+fun map_naming f =
+  map_first_lthy (fn (naming, operations, target) => (f naming, operations, target));
 
 val conceal = map_naming Name_Space.conceal;
 val new_group = map_naming Name_Space.new_group;
@@ -152,19 +155,22 @@
 val restore_naming = map_naming o K o naming_of;
 
 
-(* target *)
+(* standard morphisms *)
 
-val target_of = #target o get_lthy;
+fun standard_morphism lthy ctxt =
+  Proof_Context.norm_export_morphism lthy ctxt $>
+  Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
 
-fun map_target f = map_lthy (fn (naming, operations, target) => (naming, operations, f target));
+fun standard_form lthy ctxt x =
+  Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
 
 
-(* substructure mappings *)
+(* background theory *)
 
 fun raw_theory_result f lthy =
   let
     val (res, thy') = f (Proof_Context.theory_of lthy);
-    val lthy' = map_contexts (Proof_Context.transfer thy') lthy;
+    val lthy' = map_contexts (K (Proof_Context.transfer thy')) lthy;
   in (res, lthy') end;
 
 fun raw_theory f = #2 o raw_theory_result (f #> pair ());
@@ -181,47 +187,37 @@
 
 fun background_theory f = #2 o background_theory_result (f #> pair ());
 
-fun target_result f lthy =
+
+(* target contexts *)
+
+val target_of = #target o get_last_lthy;
+
+fun target f lthy =
   let
-    val target = target_of lthy;
-    val (res, ctxt') = target
+    val ctxt = target_of lthy;
+    val ctxt' = ctxt
       |> Context_Position.set_visible false
       |> f
-      ||> Context_Position.restore_visible target;
+      |> Context_Position.restore_visible ctxt;
     val thy' = Proof_Context.theory_of ctxt';
-    val lthy' = lthy
-      |> map_target (K ctxt')
-      |> map_contexts (Proof_Context.transfer thy');
-  in (res, lthy') end;
+  in map_contexts (fn 0 => K ctxt' | _ => Proof_Context.transfer thy') lthy end;
 
-fun target f = #2 o target_result (f #> pair ());
+fun target_morphism lthy = standard_morphism lthy (target_of lthy);
 
 fun propagate_ml_env (context as Context.Proof lthy) =
       let val inherit = ML_Env.inherit context in
         lthy
         |> background_theory (Context.theory_map inherit)
-        |> map_contexts (Context.proof_map inherit)
+        |> map_contexts (K (Context.proof_map inherit))
         |> Context.Proof
       end
   | propagate_ml_env context = context;
 
 
-(* morphisms *)
-
-fun standard_morphism lthy ctxt =
-  Proof_Context.norm_export_morphism lthy ctxt $>
-  Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
-
-fun target_morphism lthy = standard_morphism lthy (target_of lthy);
-
-fun standard_form lthy ctxt x =
-  Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
-
-
 
 (** operations **)
 
-val operations_of = #operations o get_lthy;
+val operations_of = #operations o get_first_lthy;
 
 
 (* primitives *)
@@ -252,13 +248,13 @@
 fun type_notation add mode raw_args lthy =
   let val args = map (apfst (Morphism.typ (target_morphism lthy))) raw_args in
     declaration {syntax = true, pervasive = false}
-      (Proof_Context.target_type_notation add mode args) lthy
+      (Proof_Context.generic_type_notation add mode args) lthy
   end;
 
 fun notation add mode raw_args lthy =
   let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args in
     declaration {syntax = true, pervasive = false}
-      (Proof_Context.target_notation add mode args) lthy
+      (Proof_Context.generic_notation add mode args) lthy
   end;
 
 
@@ -286,7 +282,7 @@
   |> checkpoint;
 
 fun restore lthy =
-  let val {naming, operations, target} = get_lthy lthy
+  let val {naming, operations, target} = get_first_lthy lthy
   in init naming operations target end;
 
 
diff -r bf9796e44584 -r 4c7548e7df86 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/locale.ML	Sun Apr 01 23:21:54 2012 +0200
@@ -49,8 +49,7 @@
   (* Storing results *)
   val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
     Proof.context -> Proof.context
-  val add_declaration: string -> declaration -> Proof.context -> Proof.context
-  val add_syntax_declaration: string -> declaration -> Proof.context -> Proof.context
+  val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context
 
   (* Activation *)
   val activate_declarations: string * morphism -> Proof.context -> Proof.context
@@ -536,32 +535,34 @@
 fun add_thmss _ _ [] ctxt = ctxt
   | add_thmss loc kind facts ctxt =
       ctxt
-      |> Proof_Context.note_thmss kind
-        (Attrib.map_facts (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) facts)
-      |> snd
+      |> Attrib.local_notes kind facts |> snd
       |> Proof_Context.background_theory
         ((change_locale loc o apfst o apsnd) (cons ((kind, facts), serial ())) #>
           (* Registrations *)
-          (fn thy => fold_rev (fn (_, morph) =>
-                let
-                  val facts' = facts
-                    |> Element.transform_facts morph
-                    |> Attrib.map_facts (map (Attrib.attribute_i thy));
-                in snd o Global_Theory.note_thmss kind facts' end)
+          (fn thy =>
+            fold_rev (fn (_, morph) =>
+              snd o Attrib.global_notes kind (Element.transform_facts morph facts))
             (registrations_of (Context.Theory thy) loc) thy));
 
 
 (* Declarations *)
 
-fun add_declaration loc decl =
+local
+
+fun add_decl loc decl =
   add_thmss loc ""
     [((Binding.conceal Binding.empty,
         [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
       [([Drule.dummy_thm], [])])];
 
-fun add_syntax_declaration loc decl =
-  Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
-  #> add_declaration loc decl;
+in
+
+fun add_declaration loc syntax decl =
+  syntax ?
+    Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
+  #> add_decl loc decl;
+
+end;
 
 
 (*** Reasoning about locales ***)
diff -r bf9796e44584 -r 4c7548e7df86 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/named_target.ML	Sun Apr 01 23:21:54 2012 +0200
@@ -8,7 +8,6 @@
 signature NAMED_TARGET =
 sig
   val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
-  val assert: local_theory -> local_theory
   val init: (local_theory -> local_theory) -> string -> theory -> local_theory
   val theory_init: theory -> local_theory
   val reinit: local_theory -> local_theory -> local_theory
@@ -44,35 +43,11 @@
   Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
     {target = target, is_locale = is_locale, is_class = is_class});
 
-fun assert lthy =
-  if is_some (peek lthy) then lthy
-  else error "Not in a named target (global theory, locale, class)";
 
-
-(* generic declarations *)
+(* consts in locale *)
 
-fun locale_declaration locale syntax decl lthy =
-  let
-    val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration;
-    val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
-  in
-    lthy
-    |> Local_Theory.target (add locale locale_decl)
-  end;
-
-fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy =
-  if target = "" then Generic_Target.standard_declaration decl lthy
-  else
-    lthy
-    |> pervasive ? Generic_Target.background_declaration decl
-    |> locale_declaration target syntax decl
-    |> Context.proof_map (Morphism.form decl);
-
-
-(* consts in locales *)
-
-fun locale_const (ta as Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) =
-  locale_declaration target true (fn phi =>
+fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) =
+  Generic_Target.locale_declaration target true (fn phi =>
     let
       val b' = Morphism.binding phi b;
       val rhs' = Morphism.term phi rhs;
@@ -95,7 +70,7 @@
             same_shape ?
               (Context.mapping
                 (Sign.revert_abbrev mode d) (Proof_Context.revert_abbrev mode d) #>
-               Morphism.form (Proof_Context.target_notation true prmode [(lhs', mx)]))))
+               Morphism.form (Proof_Context.generic_notation true prmode [(lhs', mx)]))))
     end);
 
 
@@ -121,21 +96,9 @@
 
 (* notes *)
 
-fun locale_notes locale kind global_facts local_facts lthy =
-  let
-    val global_facts' = Attrib.map_facts (K []) global_facts;
-    val local_facts' = local_facts
-      |> Attrib.partial_evaluation lthy
-      |> Element.transform_facts (Local_Theory.target_morphism lthy);
-  in
-    lthy
-    |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
-    |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
-  end;
-
 fun target_notes (Target {target, is_locale, ...}) =
-  if is_locale then locale_notes target
-  else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
+  if is_locale then Generic_Target.locale_notes target
+  else Generic_Target.theory_notes;
 
 
 (* abbrev *)
@@ -157,6 +120,19 @@
     |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
 
 
+(* declaration *)
+
+fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy =
+  if target = "" then Generic_Target.standard_declaration decl lthy
+  else
+    lthy
+    |> pervasive ? Generic_Target.background_declaration decl
+    |> Generic_Target.locale_declaration target syntax decl
+    |> (fn lthy' => lthy' |> Local_Theory.map_contexts (fn level => fn ctxt =>
+        if level = 0 then ctxt
+        else Context.proof_map (Local_Theory.standard_form lthy' ctxt decl) ctxt));
+
+
 (* pretty *)
 
 fun pretty (Target {target, is_locale, is_class, ...}) ctxt =
diff -r bf9796e44584 -r 4c7548e7df86 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/overloading.ML	Sun Apr 01 23:21:54 2012 +0200
@@ -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.map_contexts synchronize_syntax
+  ##> Local_Theory.map_contexts (K synchronize_syntax)
   #-> (fn (_, def) => pair (Const (c, U), def));
 
 fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
@@ -203,8 +203,7 @@
     |> synchronize_syntax
     |> Local_Theory.init naming
        {define = Generic_Target.define foundation,
-        notes = Generic_Target.notes
-          (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
+        notes = Generic_Target.notes Generic_Target.theory_notes,
         abbrev = Generic_Target.abbrev
           (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
             Generic_Target.theory_abbrev prmode ((b, mx), t)),
diff -r bf9796e44584 -r 4c7548e7df86 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Apr 01 23:21:54 2012 +0200
@@ -136,9 +136,9 @@
   val get_case: Proof.context -> string -> binding option list -> Rule_Cases.T
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
-  val target_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
+  val generic_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
     Context.generic -> Context.generic
-  val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
+  val generic_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
     Context.generic -> Context.generic
   val class_alias: binding -> class -> Proof.context -> Proof.context
   val type_alias: binding -> string -> Proof.context -> Proof.context
@@ -970,7 +970,7 @@
 val type_notation = gen_notation (K type_syntax);
 val notation = gen_notation const_syntax;
 
-fun target_type_notation add mode args phi =
+fun generic_type_notation add mode args phi =
   let
     val args' = args |> map_filter (fn (T, mx) =>
       let
@@ -979,7 +979,7 @@
       in if similar then SOME (T', mx) else NONE end);
   in Context.mapping (Sign.type_notation add mode args') (type_notation add mode args') end;
 
-fun target_notation add mode args phi =
+fun generic_notation add mode args phi =
   let
     val args' = args |> map_filter (fn (t, mx) =>
       let val t' = Morphism.term phi t
diff -r bf9796e44584 -r 4c7548e7df86 src/Tools/interpretation_with_defs.ML
--- a/src/Tools/interpretation_with_defs.ML	Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Tools/interpretation_with_defs.ML	Sun Apr 01 23:21:54 2012 +0200
@@ -23,7 +23,7 @@
       map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
         maps snd;
   in
-    Element.generic_note_thmss Thm.lemmaK
+    Attrib.generic_notes Thm.lemmaK
       (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
     #-> (fn facts => `(fn context => meta_rewrite context facts))
     #-> (fn eqns => fold (fn ((dep, morph), wits) =>