# HG changeset patch
# User paulson
# Date 1114612827 -7200
# Node ID 67574c1b15a09154a54fff353e523f6926516881
# Parent  cf2c6cf35216925441e13998b1e951825e3d3bd9
removed unnecessary (?) check

diff -r cf2c6cf35216 -r 67574c1b15a0 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Wed Apr 27 16:39:59 2005 +0200
+++ b/src/HOL/Tools/meson.ML	Wed Apr 27 16:40:27 2005 +0200
@@ -237,7 +237,7 @@
   let fun rots (0,th) = hcs
 	| rots (k,th) = zero_var_indexes (make_horn crules th) ::
 			rots(k-1, assoc_right (th RS disj_comm))
-  in case nliterals(prop_of (check_no_bool th)) of
+  in case nliterals(prop_of th) of
 	1 => th::hcs
       | n => rots(n, assoc_right th)
   end;