# HG changeset patch
# User wenzelm
# Date 1463045659 -7200
# Node ID be252979cfe50b140459d2787d229f8e6527be08
# Parent  6af03422535abdf8da0f400a731186ce42dd2b66# Parent  5c8e6a751adc7c1846e25dbabf45a1d1ba0926be
merged

diff -r 6af03422535a -r be252979cfe5 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu May 12 10:31:25 2016 +0200
+++ b/src/Pure/Isar/expression.ML	Thu May 12 11:34:19 2016 +0200
@@ -250,18 +250,19 @@
       (defs ~~ css) |> map (fn ((b, _), [c]) => (b, dest_propp c)) |> Defines
   | restore_elem (Notes notes, _) = Notes notes;
 
-fun check cs context =
+fun prep (_, pats) (ctxt, t :: ts) =
+  let val ctxt' = Variable.auto_fixes t ctxt
+  in
+    ((t, Syntax.check_props (Proof_Context.set_mode Proof_Context.mode_pattern ctxt') pats),
+      (ctxt', ts))
+  end;
+
+fun check cs ctxt =
   let
-    fun prep (_, pats) (ctxt, t :: ts) =
-      let val ctxt' = Variable.auto_fixes t ctxt
-      in
-        ((t, Syntax.check_props (Proof_Context.set_mode Proof_Context.mode_pattern ctxt') pats),
-          (ctxt', ts))
-      end;
-    val (cs', (context', _)) = fold_map prep cs
-      (context, Syntax.check_terms
-        (Proof_Context.set_mode Proof_Context.mode_schematic context) (map fst cs));
-  in (cs', context') end;
+    val (cs', (ctxt', _)) = fold_map prep cs
+      (ctxt, Syntax.check_terms
+        (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) (map fst cs));
+  in (cs', ctxt') end;
 
 in
 
@@ -438,15 +439,16 @@
 
 local
 
-fun prep_statement prep activate raw_elems raw_stmt context =
+fun prep_statement prep activate raw_elems raw_stmt ctxt =
   let
     val ((_, _, elems, concl), _) =
       prep {strict = true, do_close = false, fixed_frees = true}
-        ([], []) I raw_elems raw_stmt context;
-    val (_, context') = context
+        ([], []) I raw_elems raw_stmt ctxt;
+    val ctxt' = ctxt
       |> Proof_Context.set_stmt true
-      |> fold_map activate elems;
-  in (concl, context') end;
+      |> fold_map activate elems |> #2
+      |> Proof_Context.restore_stmt ctxt;
+  in (concl, ctxt') end;
 
 in
 
@@ -463,19 +465,20 @@
 
 local
 
-fun prep_declaration prep activate raw_import init_body raw_elems context =
+fun prep_declaration prep activate raw_import init_body raw_elems ctxt =
   let
-    val ((fixed, deps, elems, _), (parms, ctxt')) =
+    val ((fixed, deps, elems, _), (parms, ctxt0)) =
       prep {strict = false, do_close = true, fixed_frees = false}
-        raw_import init_body raw_elems (Element.Shows []) context;
+        raw_import init_body raw_elems (Element.Shows []) ctxt;
     (* Declare parameters and imported facts *)
-    val context' = context |>
-      fix_params fixed |>
-      fold (Context.proof_map o Locale.activate_facts NONE) deps;
-    val (elems', context'') = context' |>
-      Proof_Context.set_stmt true |>
-      fold_map activate elems;
-  in ((fixed, deps, elems', context''), (parms, ctxt')) end;
+    val ctxt' = ctxt
+      |> fix_params fixed
+      |> fold (Context.proof_map o Locale.activate_facts NONE) deps;
+    val (elems', ctxt'') = ctxt'
+      |> Proof_Context.set_stmt true
+      |> fold_map activate elems
+      ||> Proof_Context.restore_stmt ctxt';
+  in ((fixed, deps, elems', ctxt''), (parms, ctxt0)) end;
 
 in
 
@@ -498,21 +501,21 @@
     |> map (Morphism.term morph)
   end;
 
-fun prep_goal_expression prep expression context =
+fun prep_goal_expression prep expression ctxt =
   let
-    val thy = Proof_Context.theory_of context;
+    val thy = Proof_Context.theory_of ctxt;
 
     val ((fixed, deps, _, _), _) =
       prep {strict = true, do_close = true, fixed_frees = true} expression I []
-        (Element.Shows []) context;
+        (Element.Shows []) ctxt;
     (* proof obligations *)
     val propss = map (props_of thy) deps;
 
-    val goal_ctxt = context |>
-      fix_params fixed |>
-      (fold o fold) Variable.auto_fixes propss;
+    val goal_ctxt = ctxt
+      |> fix_params fixed
+      |> (fold o fold) Variable.auto_fixes propss;
 
-    val export = Variable.export_morphism goal_ctxt context;
+    val export = Variable.export_morphism goal_ctxt ctxt;
     val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
     val exp_term = Term_Subst.zero_var_indexes o Morphism.term export;
     val exp_typ = Logic.type_map exp_term;
diff -r 6af03422535a -r be252979cfe5 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu May 12 10:31:25 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu May 12 11:34:19 2016 +0200
@@ -13,7 +13,6 @@
   val get_global: theory -> string -> Proof.context
   type mode
   val mode_default: mode
-  val mode_stmt: mode
   val mode_pattern: mode
   val mode_schematic: mode
   val mode_abbrev: mode
@@ -21,7 +20,6 @@
   val get_mode: Proof.context -> mode
   val restore_mode: Proof.context -> Proof.context -> Proof.context
   val abbrev_mode: Proof.context -> bool
-  val set_stmt: bool -> Proof.context -> Proof.context
   val syn_of: Proof.context -> Syntax.syntax
   val tsig_of: Proof.context -> Type.tsig
   val set_defsort: sort -> Proof.context -> Proof.context
@@ -125,6 +123,8 @@
   val get_fact_single: Proof.context -> Facts.ref -> thm
   val get_thms: Proof.context -> xstring -> thm list
   val get_thm: Proof.context -> xstring -> thm
+  val set_stmt: bool -> Proof.context -> Proof.context
+  val restore_stmt: Proof.context -> Proof.context -> Proof.context
   val add_thms_dynamic: binding * (Context.generic -> thm list) ->
     Proof.context -> string * Proof.context
   val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
@@ -207,20 +207,17 @@
 
 datatype mode =
   Mode of
-   {stmt: bool,                (*inner statement mode*)
-    pattern: bool,             (*pattern binding schematic variables*)
+   {pattern: bool,             (*pattern binding schematic variables*)
     schematic: bool,           (*term referencing loose schematic variables*)
     abbrev: bool};             (*abbrev mode -- no normalization*)
 
-fun make_mode (stmt, pattern, schematic, abbrev) =
-  Mode {stmt = stmt, pattern = pattern, schematic = schematic, abbrev = abbrev};
+fun make_mode (pattern, schematic, abbrev) =
+  Mode {pattern = pattern, schematic = schematic, abbrev = abbrev};
 
-val mode_default   = make_mode (false, false, false, false);
-val mode_stmt      = make_mode (true, false, false, false);
-val mode_pattern   = make_mode (false, true, false, false);
-val mode_schematic = make_mode (false, false, true, false);
-val mode_abbrev    = make_mode (false, false, false, true);
-
+val mode_default   = make_mode (false, false, false);
+val mode_pattern   = make_mode (true, false, false);
+val mode_schematic = make_mode (false, true, false);
+val mode_abbrev    = make_mode (false, false, true);
 
 
 (** Isar proof context information **)
@@ -266,8 +263,8 @@
   (mode, syntax, tsig, consts, facts, cases));
 
 fun map_mode f =
-  map_data (fn (Mode {stmt, pattern, schematic, abbrev}, syntax, tsig, consts, facts, cases) =>
-    (make_mode (f (stmt, pattern, schematic, abbrev)), syntax, tsig, consts, facts, cases));
+  map_data (fn (Mode {pattern, schematic, abbrev}, syntax, tsig, consts, facts, cases) =>
+    (make_mode (f (pattern, schematic, abbrev)), syntax, tsig, consts, facts, cases));
 
 fun map_syntax f =
   map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
@@ -303,9 +300,6 @@
 val restore_mode = set_mode o get_mode;
 val abbrev_mode = get_mode #> (fn Mode {abbrev, ...} => abbrev);
 
-fun set_stmt stmt =
-  map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev));
-
 val syntax_of = #syntax o rep_data;
 val syn_of = Local_Syntax.syn_of o syntax_of;
 val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
@@ -1041,6 +1035,16 @@
 end;
 
 
+(* inner statement mode *)
+
+val inner_stmt =
+  Config.bool (Config.declare ("inner_stmt", @{here}) (K (Config.Bool false)));
+
+fun is_stmt ctxt = Config.get ctxt inner_stmt;
+val set_stmt = Config.put inner_stmt;
+val restore_stmt = set_stmt o is_stmt;
+
+
 (* facts *)
 
 fun add_thms_dynamic arg ctxt =
@@ -1062,8 +1066,8 @@
       fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
     val (res, ctxt') = fold_map app facts ctxt;
     val thms = Global_Theory.name_thms false false name (flat res);
-    val Mode {stmt, ...} = get_mode ctxt;
-  in ((name, thms), ctxt' |> update_thms {strict = false, index = stmt} (b, SOME thms)) end);
+    val index = is_stmt ctxt;
+  in ((name, thms), ctxt' |> update_thms {strict = false, index = index} (b, SOME thms)) end);
 
 fun put_thms index thms ctxt = ctxt
   |> map_naming (K Name_Space.local_naming)