--- a/src/Provers/hypsubst.ML Wed Jan 22 15:23:42 2020 +0100
+++ b/src/Provers/hypsubst.ML Wed Jan 22 19:17:57 2020 +0000
@@ -139,8 +139,6 @@
else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ]
handle TERM _ => [] | Match => [];
-fun bool2s true = "true" | bool2s false = "false"
-
local
in