src/Pure/Isar/toplevel.ML
changeset 21310 bfcc24fc7c46
parent 21294 5cd48242ef17
child 21506 b2a673894ce5
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Nov 11 21:13:11 2006 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Nov 11 21:13:12 2006 +0100
     1.3 @@ -161,10 +161,9 @@
     1.4  fun level (State NONE) = 0
     1.5    | level (State (SOME (node, _))) =
     1.6        (case History.current node of
     1.7 -        Theory (Context.Theory _, _) => 0
     1.8 -      | Theory (Context.Proof _, _) => 1
     1.9 -      | Proof (prf, _) => Proof.level (ProofHistory.current prf) + 1
    1.10 -      | SkipProof (h, _) => History.current h + 2);   (*different notion of proof depth!*)
    1.11 +        Theory _ => 0
    1.12 +      | Proof (prf, _) => Proof.level (ProofHistory.current prf)
    1.13 +      | SkipProof (h, _) => History.current h + 1);   (*different notion of proof depth!*)
    1.14  
    1.15  fun str_of_state (State NONE) = "at top level"
    1.16    | str_of_state (State (SOME (node, _))) =