src/HOL/Tools/meson.ML
changeset 15862 67574c1b15a0
parent 15779 aed221aff642
child 15872 8336ff711d80
--- 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;