| changeset 40110 | 93e7935d4cb5 |
| parent 39866 | 5ec01d5acd0c |
| child 43564 | 9864182c6bad |
--- a/doc-src/IsarImplementation/Thy/Base.thy Mon Oct 25 11:01:00 2010 +0200 +++ b/doc-src/IsarImplementation/Thy/Base.thy Mon Oct 25 11:16:23 2010 +0200 @@ -3,10 +3,4 @@ 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