# HG changeset patch
# User wenzelm
# Date 1166137696 -3600
# Node ID a972053ed1474951e6b2ea546c5e487f5547f314
# Parent  c4492c6bf4504f3fe56197d09e696951ebb384f4
removed obsolete assert;

diff -r c4492c6bf450 -r a972053ed147 src/Pure/Isar/toplevel.ML
--- 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;