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 74290 b2ad24b5a42c
parent 74282 c2ee8d993d6a
child 74610 87fc10f5826c 
--- a/src/HOL/Tools/sat.ML	Fri Sep 10 23:18:51 2021 +0200
+++ b/src/HOL/Tools/sat.ML	Sat Sep 11 13:04:32 2021 +0200
@@ -171,8 +171,7 @@
                 val cLit =
                   snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1))  (* strip Trueprop *)
               in
-                Thm.instantiate (TVars.empty, Vars.make [((("P", 0), HOLogic.boolT), cLit)])
-                  resolution_thm
+                Thm.instantiate (TVars.empty, Vars.make [(\<^var>\<open>?P::bool\<close>, cLit)]) resolution_thm
               end
 
             val _ =
isabelle