--- 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;
--- 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)