diff -r 58ddd7c5c84e -r a3ae93ed7b1b src/Provers/hypsubst.ML
--- 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