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.
clauses counted from 0
authorpaulson
Thu, 02 Dec 2004 16:02:29 +0100
changeset 15365 611c32b7f6e5
parent 15364 0c3891c3528f
child 15366 e6f595009734
clauses counted from 0
src/HOL/Tools/reconstruction.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/reconstruction.ML	Thu Dec 02 14:47:07 2004 +0100
+++ b/src/HOL/Tools/reconstruction.ML	Thu Dec 02 16:02:29 2004 +0100
@@ -168,7 +168,7 @@
 fun clausify_rule (A,i) =
   standard
     (make_meta_clause
-      (List.nth(ResAxioms.cnf_axiom A,i-1)));
+      (List.nth(ResAxioms.cnf_axiom A,i)));
 
 fun clausify_syntax i (x, A) = (x, clausify_rule (A,i));
isabelle