# HG changeset patch
# User wenzelm
# Date 1333470134 -7200
# Node ID 1addbe2a7458e1449339391eb51b9e0e0e061a57
# Parent  610d9c212376216d33df1355799155bf11bbe400
close context elements via Expression.cert/read_declaration;
ensure visible context;

diff -r 610d9c212376 -r 1addbe2a7458 src/HOL/Isar_Examples/Group_Context.thy
--- a/src/HOL/Isar_Examples/Group_Context.thy	Tue Apr 03 17:48:16 2012 +0200
+++ b/src/HOL/Isar_Examples/Group_Context.thy	Tue Apr 03 18:22:14 2012 +0200
@@ -14,9 +14,9 @@
   fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "**" 70)
     and one :: "'a"
     and inverse :: "'a => 'a"
-  assumes assoc: "\<And>x y z. (x ** y) ** z = x ** (y ** z)"
-    and left_one: "\<And>x. one ** x = x"
-    and left_inverse: "\<And>x. inverse x ** x = one"
+  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
+    and left_one: "one ** x = x"
+    and left_inverse: "inverse x ** x = one"
 begin
 
 text {* some consequences *}
diff -r 610d9c212376 -r 1addbe2a7458 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Tue Apr 03 17:48:16 2012 +0200
+++ b/src/Pure/Isar/bundle.ML	Tue Apr 03 18:22:14 2012 +0200
@@ -91,10 +91,16 @@
   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_bundle prep_stmt raw_incls raw_elems gthy =
+fun gen_context prep_bundle prep_decl 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;
+    fun augment ctxt =
+      let
+        val ((_, _, _, ctxt'), _) = ctxt
+          |> Context_Position.set_visible true
+          |> gen_includes prep_bundle raw_incls
+          |> prep_decl ([], []) I raw_elems;
+      in ctxt' |> Context_Position.restore_visible ctxt end;
   in
     (case gthy of
       Context.Theory _ => Local_Theory.target augment lthy |> Local_Theory.restore
@@ -115,8 +121,8 @@
 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;
+val context = gen_context (K I) Expression.cert_declaration;
+val context_cmd = gen_context check Expression.read_declaration;
 
 end;
 
diff -r 610d9c212376 -r 1addbe2a7458 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Tue Apr 03 17:48:16 2012 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Tue Apr 03 18:22:14 2012 +0200
@@ -157,7 +157,7 @@
       fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
       #> Class.redeclare_operations thy sups
       #> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" (K singleton_fixate));
-    val ((raw_supparams, _, raw_inferred_elems), _) =
+    val ((raw_supparams, _, raw_inferred_elems, _), _) =
       Proof_Context.init_global thy
       |> Context.proof_map (Syntax_Phases.term_check 0 "after_infer_fixate" (K after_infer_fixate))
       |> prep_decl raw_supexpr init_class_body raw_elems;
@@ -221,7 +221,7 @@
 
     (* process elements as class specification *)
     val class_ctxt = Class.begin sups base_sort thy_ctxt;
-    val ((_, _, syntax_elems), _) = class_ctxt
+    val ((_, _, syntax_elems, _), _) = class_ctxt
       |> Expression.cert_declaration supexpr I inferred_elems;
     fun check_vars e vs =
       if null vs then
diff -r 610d9c212376 -r 1addbe2a7458 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Tue Apr 03 17:48:16 2012 +0200
+++ b/src/Pure/Isar/expression.ML	Tue Apr 03 18:22:14 2012 +0200
@@ -21,14 +21,14 @@
   (* Declaring locales *)
   val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list ->
     Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
-      * Element.context_i list) * ((string * typ) list * Proof.context)
+      * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
   val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context list ->
     Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
-      * Element.context_i list) * ((string * typ) list * Proof.context)
+      * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
       (*FIXME*)
   val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
     Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
-      * Element.context_i list) * ((string * typ) list * Proof.context)
+      * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
   val add_locale: (local_theory -> local_theory) -> binding -> binding ->
     expression_i -> Element.context_i list -> theory -> string * local_theory
   val add_locale_cmd: (local_theory -> local_theory) -> binding -> binding ->
@@ -458,10 +458,10 @@
     val context' = context |>
       fix_params fixed |>
       fold (Context.proof_map o Locale.activate_facts NONE) deps;
-    val (elems', _) = context' |>
+    val (elems', context'') = context' |>
       Proof_Context.set_stmt true |>
       fold_map activate elems;
-  in ((fixed, deps, elems'), (parms, ctxt')) end;
+  in ((fixed, deps, elems', context''), (parms, ctxt')) end;
 
 in
 
@@ -735,7 +735,7 @@
     val _ = Locale.defined thy name andalso
       error ("Duplicate definition of locale " ^ quote name);
 
-    val ((fixed, deps, body_elems), (parms, ctxt')) =
+    val ((fixed, deps, body_elems, _), (parms, ctxt')) =
       prep_decl raw_import I raw_body (Proof_Context.init_global thy);
     val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;