diff -r a724b90f951e -r 5ec01d5acd0c doc-src/IsarImplementation/Thy/Base.thy
--- a/doc-src/IsarImplementation/Thy/Base.thy	Mon Oct 18 16:23:55 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Base.thy	Mon Oct 18 19:06:07 2010 +0100
@@ -3,4 +3,10 @@
 uses "../../antiquote_setup.ML"
 begin
 
+(* FIXME move to src/Pure/ML/ml_antiquote.ML *)
+ML {*
+  ML_Antiquote.inline "assert"
+    (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")")
+*}
+
 end