--- a/src/Pure/Isar/toplevel.ML Fri Dec 15 00:08:15 2006 +0100
+++ b/src/Pure/Isar/toplevel.ML Fri Dec 15 00:08:16 2006 +0100
@@ -20,7 +20,6 @@
val is_theory: state -> bool
val is_proof: state -> bool
val level: state -> int
- val assert: bool -> unit
val node_history_of: state -> node History.T
val node_of: state -> node
val node_case: (generic_theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
@@ -176,9 +175,6 @@
(* top node *)
-fun assert true = ()
- | assert false = raise UNDEF;
-
fun node_history_of (State NONE) = raise UNDEF
| node_history_of (State (SOME (node, _))) = node;