src/Pure/Isar/toplevel.ML
changeset 16490 e10b0d5fa33a
parent 16452 71f3e0041f14
child 16607 81e687c63e29
--- a/src/Pure/Isar/toplevel.ML	Mon Jun 20 22:14:03 2005 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Jun 20 22:14:04 2005 +0200
@@ -7,8 +7,7 @@
 
 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
@@ -228,8 +227,7 @@
       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;