--- a/NEWS Fri Feb 26 22:38:44 2016 +0100
+++ b/NEWS Sat Mar 05 12:49:47 2016 +0100
@@ -189,6 +189,14 @@
debugger information requires consirable time and space: main
Isabelle/HOL with full debugger support may need ML_system_64.
+* Local_Theory.restore has been renamed to Local_Theory.reset to
+emphasize its disruptive impact on the cumulative context, notably the
+scope of 'private' or 'qualified' names. Note that Local_Theory.reset is
+only appropriate when targets are managed, e.g. starting from a global
+theory and returning to it. Regular definitional packages should use
+balanced blocks of Local_Theory.open_target versus
+Local_Theory.close_target instead. Rare INCOMPATIBILITY.
+
*** System ***
--- a/src/HOL/Library/bnf_axiomatization.ML Fri Feb 26 22:38:44 2016 +0100
+++ b/src/HOL/Library/bnf_axiomatization.ML Sat Mar 05 12:49:47 2016 +0100
@@ -83,7 +83,7 @@
val (((_, [raw_thms])), (lthy_old, lthy)) = Local_Theory.background_theory_result
(Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy
- ||> `Local_Theory.restore;
+ ||> `Local_Theory.reset;
fun mk_wit_thms set_maps =
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
--- a/src/HOL/Tools/Lifting/lifting_def.ML Fri Feb 26 22:38:44 2016 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Sat Mar 05 12:49:47 2016 +0100
@@ -610,7 +610,7 @@
lthy
|> Local_Theory.notes (notes (#notes config)) |> snd
|> ` (fn lthy => morph_lift_def (Local_Theory.target_morphism lthy) lift_def)
- ||> Local_Theory.restore
+ ||> Local_Theory.reset
end
(* This is not very cheap way of getting the rules but we have only few active
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Fri Feb 26 22:38:44 2016 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sat Mar 05 12:49:47 2016 +0100
@@ -211,7 +211,7 @@
handle THM _ => error ("code_dt: " ^ quote (Tname qty) ^ " was not defined as a subtype."))
val code_dt = mk_code_dt rty qty wit wit_thm NONE
in
- (quot_thm, (update_code_dt code_dt lthy |> Local_Theory.restore, rel_eq_onps))
+ (quot_thm, (update_code_dt code_dt lthy |> Local_Theory.reset, rel_eq_onps))
end
else
(quot_thm, (lthy, rel_eq_onps))
@@ -340,7 +340,7 @@
val lthy = lthy
|> Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => fn context => Data.map (Item_Net.update (morph_code_dt phi (code_dt phi context))) context)
- |> Local_Theory.restore
+ |> Local_Theory.reset
(* in order to make the qty qty_isom isomorphism executable we have to define discriminators
and selectors for qty_isom *)
@@ -571,12 +571,12 @@
val config = { notes = false}
val (binding, lthy) = conceal_naming_result (Lifting_Setup.setup_by_typedef_thm
config type_definition_thm) lthy
- val lthy = Local_Theory.restore lthy
+ val lthy = Local_Theory.reset lthy
val (wit, wit_thm) = mk_witness quot_thm;
val code_dt = mk_code_dt rty qty wit wit_thm NONE;
val lthy = lthy
|> update_code_dt code_dt
- |> Local_Theory.restore
+ |> Local_Theory.reset
|> mk_rep_isom binding (rty, qty, qty_isom) |> snd
in
(quot_thm, (lthy, rel_eq_onps))
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Feb 26 22:38:44 2016 +0100
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Sat Mar 05 12:49:47 2016 +0100
@@ -215,7 +215,7 @@
|> snd
|> Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data))
- |> Local_Theory.restore
+ |> Local_Theory.reset
end
(* BNF interpretation *)
@@ -268,7 +268,7 @@
lthy
|> Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data))
- |> Local_Theory.restore
+ |> Local_Theory.reset
end
fun transfer_fp_sugars_interpretation fp_sugar lthy =
--- a/src/Pure/Isar/local_theory.ML Fri Feb 26 22:38:44 2016 +0100
+++ b/src/Pure/Isar/local_theory.ML Sat Mar 05 12:49:47 2016 +0100
@@ -16,7 +16,7 @@
sig
type operations
val assert: local_theory -> local_theory
- val restore: local_theory -> local_theory
+ val reset: local_theory -> local_theory
val level: Proof.context -> int
val assert_bottom: bool -> local_theory -> local_theory
val mark_brittle: local_theory -> local_theory
@@ -132,7 +132,7 @@
Data.map (fn {background_naming, operations, after_close, brittle, target} :: parents =>
make_lthy (f (background_naming, operations, after_close, brittle, target)) :: parents);
-fun restore lthy = #target (top_of lthy) |> Data.put (Data.get lthy);
+fun reset lthy = #target (top_of lthy) |> Data.put (Data.get lthy);
(* nested structure *)
@@ -388,6 +388,6 @@
let
val _ = assert_bottom false lthy;
val ({after_close, ...} :: rest) = Data.get lthy;
- in lthy |> Data.put rest |> restore |> after_close end;
+ in lthy |> Data.put rest |> reset |> after_close end;
end;
--- a/src/Pure/Isar/named_target.ML Fri Feb 26 22:38:44 2016 +0100
+++ b/src/Pure/Isar/named_target.ML Sat Mar 05 12:49:47 2016 +0100
@@ -176,7 +176,7 @@
| switch (SOME name) (Context.Theory thy) =
(Context.Theory o exit, begin name thy)
| switch NONE (Context.Proof lthy) =
- (Context.Proof o Local_Theory.restore, lthy)
+ (Context.Proof o Local_Theory.reset, lthy)
| switch (SOME name) (Context.Proof lthy) =
(Context.Proof o init (target_of lthy) o exit,
(begin name o exit o Local_Theory.assert_nonbrittle) lthy);