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_solver.ML
changeset 77888 3c837f8c8ed5
parent 75615 4494cd69f97f
child 77896 a9626bcb0c3b 
--- a/src/HOL/Tools/sat_solver.ML	Wed Apr 19 23:27:33 2023 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Wed Apr 19 23:27:55 2023 +0200
@@ -682,7 +682,7 @@
             original_clause_id_from 0
           (* both 'lits' and the list of literals used in 'clauses' are sorted, so *)
           (* testing for equality should suffice -- barring duplicate literals     *)
-          else if Array.sub (clauses, index) = lits then (
+          else if Array.nth clauses index = lits then (
             (* success *)
             last_ref_clause := index;
             SOME index
isabelle