Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clausification bug fix
authorpaulson
Wed, 01 Jun 2005 18:19:59 +0200
changeset 16173 9e2f6c0a779d
parent 16172 629ba53a072f
child 16174 a55c796b1f79
clausification bug fix
src/HOL/Tools/meson.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/res_axioms.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/meson.ML	Wed Jun 01 14:50:48 2005 +0200
+++ b/src/HOL/Tools/meson.ML	Wed Jun 01 18:19:59 2005 +0200
@@ -160,7 +160,7 @@
 
 (*Convert all suitable free variables to schematic variables, 
   but don't discharge assumptions.*)
-fun generalize th = forall_elim_vars 0 (forall_intr_frees th);
+fun generalize th = Thm.varifyT (forall_elim_vars 0 (forall_intr_frees th));
 
 fun make_cnf skoths th = map generalize (cnf skoths (th, []));
 
--- a/src/HOL/Tools/res_axioms.ML	Wed Jun 01 14:50:48 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Wed Jun 01 18:19:59 2005 +0200
@@ -187,7 +187,7 @@
 
 (* transform an Isabelle thm into CNF *)
 fun cnf_axiom_aux th =
-    map (zero_var_indexes o Thm.varifyT) 
+    map zero_var_indexes
         (rm_redundant_cls (cnf_rule (transfer_to_Reconstruction th)));
isabelle