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;