tuned;

--- a/src/HOL/Tools/sat_funcs.ML	Wed Mar 27 11:54:53 2013 +0100
+++ b/src/HOL/Tools/sat_funcs.ML	Wed Mar 27 14:08:03 2013 +0100
@@ -324,14 +324,13 @@
         tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms))
       else ()
     val fm = Prop_Logic.all fms
-    (* unit -> Thm.thm *)
     fun make_quick_and_dirty_thm () =
       let
         val _ =
           if !trace_sat then
             tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
           else ()
-        val False_thm = Skip_Proof.make_thm @{theory} (HOLogic.Trueprop $ @{term False})
+        val False_thm = Skip_Proof.make_thm_cterm @{cprop False}
       in
         (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold    *)
         (* Thm.weaken sorted_clauses' would be quadratic, since we sorted   *)