Fix variable-naming bug (?) by removing a needless recursive call
authorpaulson
Mon, 20 Feb 2006 16:22:52 +0100
changeset 19112 f81f8706cd37
parent 19111 1f6112de1d0f
child 19113 2cb4559782f4
Fix variable-naming bug (?) by removing a needless recursive call
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,