# HG changeset patch
# User haftmann
# Date 1579720677 0
# Node ID a3ae93ed7b1b4822c4b8466bee479736b930e9b8
# Parent  58ddd7c5c84e9ae63f93536168f6da86be62c5f1
dropped dead code

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