author | paulson |
Mon, 20 Feb 2006 16:22:52 +0100 | |
changeset 19112 | f81f8706cd37 |
parent 19111 | 1f6112de1d0f |
child 19113 | 2cb4559782f4 |
--- 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,