# HG changeset patch
# User paulson
# Date 1140448972 -3600
# Node ID f81f8706cd376829ba31c33d74a86874ed4363b8
# Parent  1f6112de1d0f7309f392e9a2875df2a71ac5e260
Fix variable-naming bug (?) by removing a needless recursive call

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,