# HG changeset patch # User wenzelm # Date 1333374170 -7200 # Node ID b0b78ce6903a9cf29879e03066cf12084d3c59c0 # Parent 2511f3e8449628040b6e3bc41acb09765b001fd5 more general Local_Theory.restore, allow any nesting level; diff -r 2511f3e84496 -r b0b78ce6903a src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Mon Apr 02 13:47:00 2012 +0200 +++ b/src/Pure/Isar/local_theory.ML Mon Apr 02 15:42:50 2012 +0200 @@ -33,6 +33,7 @@ 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 restore: local_theory -> local_theory val operations_of: local_theory -> operations val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory @@ -54,7 +55,6 @@ val type_alias: binding -> string -> local_theory -> local_theory val const_alias: binding -> string -> local_theory -> local_theory val init: Name_Space.naming -> operations -> Proof.context -> local_theory - val restore: local_theory -> local_theory val exit: local_theory -> Proof.context val exit_global: local_theory -> theory val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context @@ -213,6 +213,8 @@ end | propagate_ml_env context = context; +fun restore lthy = target_of lthy |> Data.put (Data.get lthy); + (** operations **) @@ -281,10 +283,6 @@ | _ => error "Local theory already initialized") |> checkpoint; -fun restore lthy = - let val {naming, operations, target} = get_first_lthy lthy - in init naming operations target end; - (* exit *)