author | paulson |
Wed, 27 Apr 2005 16:40:27 +0200 | |
changeset 15862 | 67574c1b15a0 |
parent 15861 | cf2c6cf35216 |
child 15863 | 78db9506cc78 |
--- 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;