# HG changeset patch
# User wenzelm
# Date 1633510685 -7200
# Node ID 7cc59201157d267f1c7e85e50768beff215ea548
# Parent  b3d6bb2ebf77c1c4478c82e76dafc30cd84e383b
clarified signature;

diff -r b3d6bb2ebf77 -r 7cc59201157d src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Oct 05 15:44:10 2021 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Oct 06 10:58:05 2021 +0200
@@ -10,7 +10,7 @@
   type state
   val init_toplevel: unit -> state
   val theory_toplevel: theory -> state
-  val get_prev_theory: generic_theory -> serial
+  val get_prev_theory: theory -> serial
   val is_toplevel: state -> bool
   val is_theory: state -> bool
   val is_proof: state -> bool
@@ -148,7 +148,7 @@
 fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), NONE);
 
 val prev_theory = Config.declare_int ("prev_theory", Position.none) (K 0);
-fun get_prev_theory gthy = Config.get_global (Context.theory_of gthy) prev_theory;
+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);