# HG changeset patch
# User wenzelm
# Date 1644938213 -3600
# Node ID 32947e5c453dc185332acec3a9492ed4c0da751c
# Parent  3bcbc4d12916b6fba1c6e2698e31bcf2c10000af
obsolete (reverting b3d6bb2ebf77): Isabelle/Naproche cache is now value-oriented;

diff -r 3bcbc4d12916 -r 32947e5c453d src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Feb 14 16:41:48 2022 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Feb 15 16:16:53 2022 +0100
@@ -10,7 +10,6 @@
   type state
   val init_toplevel: unit -> state
   val theory_toplevel: theory -> state
-  val get_prev_theory: theory -> serial
   val is_toplevel: state -> bool
   val is_theory: state -> bool
   val is_proof: state -> bool
@@ -153,15 +152,6 @@
 fun init_toplevel () = State (node_presentation Toplevel, (NONE, NONE));
 fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), (NONE, NONE));
 
-val prev_theory = Config.declare_int ("prev_theory", Position.none) (K 0);
-fun get_prev_theory thy = Config.get_global thy prev_theory;
-fun set_prev_theory (State (_, (SOME prev_thy, _))) (Theory gthy) =
-      let
-        val put = Config.put_global prev_theory (Context.theory_identifier prev_thy);
-        val gthy' = gthy |> Context.mapping put (Local_Theory.raw_theory put);
-      in Theory gthy' end
-  | set_prev_theory _ node = node;
-
 fun level state =
   (case node_of state of
     Toplevel => 0
@@ -329,7 +319,7 @@
             val state' = State (node_presentation node, (prev_thy, NONE));
           in apply_presentation (fn st => f int st) state' end) ()
   | (Transaction _, Toplevel) => raise UNDEF
-  | (Transaction (f, g), node) => apply (fn x => f int x) g (set_prev_theory state node)
+  | (Transaction (f, g), node) => apply (fn x => f int x) g node
   | _ => raise UNDEF);
 
 fun apply_union _ [] state = raise FAILURE (state, UNDEF)