src/Pure/goal.ML
changeset 52059 2f970c7f722b
parent 51958 bca32217b304
child 52104 250cd2a9308d
--- a/src/Pure/goal.ML	Fri May 17 20:30:04 2013 +0200
+++ b/src/Pure/goal.ML	Fri May 17 20:41:45 2013 +0200
@@ -337,7 +337,7 @@
   Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);
 
 fun prove_sorry ctxt xs asms prop tac =
-  if ! quick_and_dirty then
+  if Config.get ctxt quick_and_dirty then
     prove ctxt xs asms prop (fn _ => ALLGOALS Skip_Proof.cheat_tac)
   else (if future_enabled () then prove_future else prove) ctxt xs asms prop tac;