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/ex/SAT_Examples.thy
changeset 59643 f3be9235503d
parent 59621 291934bac95e
child 61343 5b5656a63bd6 
--- a/src/HOL/ex/SAT_Examples.thy	Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/ex/SAT_Examples.thy	Fri Mar 06 23:57:01 2015 +0100
@@ -534,7 +534,7 @@
         | and_to_list fm acc = rev (fm :: acc)
       val clauses = and_to_list prop_fm []
       val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
-      val cterms = map (Thm.global_cterm_of @{theory}) terms
+      val cterms = map (Thm.cterm_of @{context}) terms
       val start = Timing.start ()
       val _ = SAT.rawsat_thm @{context} cterms
     in
isabelle