src/Pure/Isar/toplevel.ML

 The Isabelle/Isar toplevel.
 *)
 
 signature TOPLEVEL =
 sig
-  datatype node = Theory of theory | Proof of ProofHistory.T
-    | SkipProof of int History.T * theory
+  datatype node = Theory of theory | Proof of ProofHistory.T | SkipProof of int History.T * theory
   type state
   val toplevel: state
   val is_toplevel: state -> bool
   val prompt_state_default: state -> string
   val prompt_state_fn: (state -> string) ref

         if is_stale result then return (mk_state back_node, SOME (if_none opt_exn rollback))
         else return (result, opt_exn)
       end;
 
 fun check_stale state =
-  if not (is_stale state) then ()
-  else warning "Stale theory encountered!";
+  conditional (is_stale state) (fn () => warning "Stale theory encountered!");
 
 end;
 
 
 (* primitive transitions *)