src/Pure/Isar/local_theory.ML

   val group_position_of: local_theory -> Properties.T
   val set_group: string -> local_theory -> local_theory
   val target_of: local_theory -> Proof.context
   val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val raw_theory: (theory -> theory) -> local_theory -> local_theory
+  val checkpoint: local_theory -> local_theory
   val full_naming: local_theory -> NameSpace.naming
   val full_name: local_theory -> bstring -> string
   val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val theory: (theory -> theory) -> local_theory -> local_theory
   val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory

       |> ProofContext.transfer thy';
   in (res, lthy') end;
 
 fun raw_theory f = #2 o raw_theory_result (f #> pair ());
 
+val checkpoint = raw_theory Theory.checkpoint;
+
 fun full_naming lthy =
   Sign.naming_of (ProofContext.theory_of lthy)
   |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy))
   |> NameSpace.qualified_names;
 

 fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
 fun operation1 f x = operation (fn ops => f ops x);
 fun operation2 f x y lthy = operation (fn ops => f ops x y) lthy;
 
 val pretty = operation #pretty;
-val abbrev = operation2 #abbrev;
-val define = operation2 #define;
-val notes = operation2 #notes;
-val type_syntax = operation1 #type_syntax;
-val term_syntax = operation1 #term_syntax;
-val declaration = operation1 #declaration;
+val abbrev = apsnd checkpoint ooo operation2 #abbrev;
+val define = apsnd checkpoint ooo operation2 #define;
+val notes = apsnd checkpoint ooo operation2 #notes;
+val type_syntax = checkpoint oo operation1 #type_syntax;
+val term_syntax = checkpoint oo operation1 #term_syntax;
+val declaration = checkpoint oo operation1 #declaration;
 
 fun note kind (a, ths) = notes kind [(a, [(ths, [])])] #>> the_single;
 
 fun target_morphism lthy =
   ProofContext.export_morphism lthy (target_of lthy) $>

 
 (* init -- exit *)
 
 fun init theory_prefix operations target = target |> Data.map
   (fn NONE => SOME (make_lthy ("", theory_prefix, operations, target))
-    | SOME _ => error "Local theory already initialized");
+    | SOME _ => error "Local theory already initialized")
+  |> checkpoint;
 
 fun restore lthy =
   let val {group = _, theory_prefix, operations, target} = get_lthy lthy
   in init theory_prefix operations target end;
 
-val reinit = operation #reinit;
-val exit = operation #exit;
+val reinit = checkpoint o operation #reinit;
+val exit = ProofContext.theory Theory.checkpoint o operation #exit;
 
 end;