--- a/src/HOL/Tools/sat.ML Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Tools/sat.ML Fri Mar 06 15:58:56 2015 +0100
@@ -73,7 +73,7 @@
val resolution_thm =
@{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
-val cP = Thm.cterm_of @{theory} (Var (("P", 0), HOLogic.boolT));
+val cP = Thm.global_cterm_of @{theory} (Var (("P", 0), HOLogic.boolT));
(* ------------------------------------------------------------------------- *)
(* lit_ord: an order on integers that considers their absolute values only, *)