src/Pure/Isar/toplevel.ML
changeset 67391 d55e52e25d9a
parent 67390 a256051dd3d6
child 67392 1256460c063a
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Jan 09 17:58:35 2018 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Jan 09 18:18:21 2018 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4    val is_proof: state -> bool
     1.5    val is_skipped_proof: state -> bool
     1.6    val level: state -> int
     1.7 -  val previous_context_of: state -> Proof.context option
     1.8 +  val previous_theory_of: state -> theory option
     1.9    val context_of: state -> Proof.context
    1.10    val generic_theory_of: state -> generic_theory
    1.11    val theory_of: state -> theory
    1.12 @@ -153,8 +153,9 @@
    1.13  
    1.14  fun node_case f g state = cases_node f g (node_of state);
    1.15  
    1.16 -fun previous_context_of (State (_, NONE)) = NONE
    1.17 -  | previous_context_of (State (_, SOME prev)) = SOME (context_node prev);
    1.18 +fun previous_theory_of (State (_, NONE)) = NONE
    1.19 +  | previous_theory_of (State (_, SOME prev)) =
    1.20 +      SOME (cases_node Context.theory_of Proof.theory_of prev);
    1.21  
    1.22  val context_of = node_case Context.proof_of Proof.context_of;
    1.23  val generic_theory_of = node_case I (Context.Proof o Proof.context_of);