Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/sat.ML
changeset 77888 3c837f8c8ed5
parent 77872 c404695aaf95
child 77896 a9626bcb0c3b 
--- a/src/HOL/Tools/sat.ML	Wed Apr 19 23:27:33 2023 +0200
+++ b/src/HOL/Tools/sat.ML	Wed Apr 19 23:27:55 2023 +0200
@@ -216,7 +216,7 @@
       handle TERM _ => NONE;  (* 'chyp' is not a literal *)
 
     fun prove_clause id =
-      (case Array.sub (clauses, id) of
+      (case Array.nth clauses id of
         RAW_CLAUSE clause => clause
       | ORIG_CLAUSE thm =>
           (* convert the original clause *)
isabelle