# HG changeset patch
# User wenzelm
# Date 1564321170 -7200
# Node ID 495881aadbff5f5181e48102f180f2c9e14c24b0
# Parent  dbb32c2d5c2c1a2a6484e0ad51a83e81ebe86d98
purge remains from test (cf. 5a53724fe247);

diff -r dbb32c2d5c2c -r 495881aadbff src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Sun Jul 28 14:37:32 2019 +0200
+++ b/src/FOL/IFOL.thy	Sun Jul 28 15:39:30 2019 +0200
@@ -8,7 +8,6 @@
 imports Pure
 begin
 
-ML \<open>\<^assert> (not (can ML \<open>open RunCall\<close>))\<close>
 ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
 ML_file \<open>~~/src/Provers/splitter.ML\<close>
 ML_file \<open>~~/src/Provers/hypsubst.ML\<close>