tuned signature -- clarified modules;

--- a/src/Pure/Isar/attrib.ML	Fri Oct 30 16:31:37 2015 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Oct 30 17:14:30 2015 +0100
@@ -510,7 +510,7 @@
 (* theory setup *)
 
 val _ = Theory.setup
- (register_config quick_and_dirty_raw #>
+ (register_config Goal.quick_and_dirty_raw #>
   register_config Ast.trace_raw #>
   register_config Ast.stats_raw #>
   register_config Printer.show_brackets_raw #>

--- a/src/Pure/goal.ML	Fri Oct 30 16:31:37 2015 +0100
+++ b/src/Pure/goal.ML	Fri Oct 30 17:14:30 2015 +0100
@@ -6,6 +6,7 @@
 
 signature BASIC_GOAL =
 sig
+  val quick_and_dirty: bool Config.T
   val parallel_proofs: int Unsynchronized.ref
   val SELECT_GOAL: tactic -> int -> tactic
   val PREFER_GOAL: tactic -> int -> tactic
@@ -38,6 +39,7 @@
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
   val prove_global: theory -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
+  val quick_and_dirty_raw: Config.raw
   val prove_sorry: Proof.context -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
   val prove_sorry_global: theory -> string list -> term list -> term ->
@@ -250,6 +252,12 @@
 fun prove_global thy xs asms prop tac =
   Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);
 
+
+(* skip proofs *)
+
+val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", @{here});
+val quick_and_dirty = Config.bool quick_and_dirty_raw;
+
 fun prove_sorry ctxt xs asms prop tac =
   if Config.get ctxt quick_and_dirty then
     prove ctxt xs asms prop (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt))

--- a/src/Pure/skip_proof.ML	Fri Oct 30 16:31:37 2015 +0100
+++ b/src/Pure/skip_proof.ML	Fri Oct 30 17:14:30 2015 +0100
@@ -4,9 +4,6 @@
 Skip proof via oracle invocation.
 *)
 
-val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", @{here});
-val quick_and_dirty = Config.bool quick_and_dirty_raw;
-
 signature SKIP_PROOF =
 sig
   val report: Proof.context -> unit