clarified signature;
authorwenzelm
Tue Jan 09 18:18:21 2018 +0100 (17 months ago ago)
changeset 67391d55e52e25d9a
parent 67390 a256051dd3d6
child 67392 1256460c063a
clarified signature;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Jan 09 17:58:35 2018 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Jan 09 18:18:21 2018 +0100
     1.3 @@ -226,8 +226,8 @@
     1.4      let
     1.5        val ctxt = Toplevel.context_of st;
     1.6        val prev_thys =
     1.7 -        (case Toplevel.previous_context_of st of
     1.8 -          SOME prev => [Proof_Context.theory_of prev]
     1.9 +        (case Toplevel.previous_theory_of st of
    1.10 +          SOME thy => [thy]
    1.11          | NONE => Theory.parents_of (Proof_Context.theory_of ctxt));
    1.12      in Proof_Display.pretty_theorems_diff verbose prev_thys ctxt end;
    1.13  
     2.1 --- a/src/Pure/Isar/toplevel.ML	Tue Jan 09 17:58:35 2018 +0100
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Jan 09 18:18:21 2018 +0100
     2.3 @@ -15,7 +15,7 @@
     2.4    val is_proof: state -> bool
     2.5    val is_skipped_proof: state -> bool
     2.6    val level: state -> int
     2.7 -  val previous_context_of: state -> Proof.context option
     2.8 +  val previous_theory_of: state -> theory option
     2.9    val context_of: state -> Proof.context
    2.10    val generic_theory_of: state -> generic_theory
    2.11    val theory_of: state -> theory
    2.12 @@ -153,8 +153,9 @@
    2.13  
    2.14  fun node_case f g state = cases_node f g (node_of state);
    2.15  
    2.16 -fun previous_context_of (State (_, NONE)) = NONE
    2.17 -  | previous_context_of (State (_, SOME prev)) = SOME (context_node prev);
    2.18 +fun previous_theory_of (State (_, NONE)) = NONE
    2.19 +  | previous_theory_of (State (_, SOME prev)) =
    2.20 +      SOME (cases_node Context.theory_of Proof.theory_of prev);
    2.21  
    2.22  val context_of = node_case Context.proof_of Proof.context_of;
    2.23  val generic_theory_of = node_case I (Context.Proof o Proof.context_of);