diff -r 1f6112de1d0f -r f81f8706cd37 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Mon Feb 20 11:38:06 2006 +0100
+++ b/src/HOL/Tools/meson.ML	Mon Feb 20 16:22:52 2006 +0100
@@ -210,8 +210,7 @@
       and cnf_nil th = (cnf_aux (th,[]))
   in 
     name_ref := 19;  (*It's safe to reset this in a top-level call to cnf*)
-    (cnf skoths (th RS conjunct1, cnf skoths (th RS conjunct2, ths))
-     handle THM _ => (*not a conjunction*) cnf_aux (th, ths))
+    cnf_aux (th,ths)
   end;
 
 (*Convert all suitable free variables to schematic variables,