removed unnecessary (?) check
authorpaulson
Wed, 27 Apr 2005 16:40:27 +0200
changeset 15862 67574c1b15a0
parent 15861 cf2c6cf35216
child 15863 78db9506cc78
removed unnecessary (?) check
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;