tuned;

--- a/src/Pure/Isar/toplevel.ML	Mon Jul 04 17:07:15 2005 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Jul 04 17:08:19 2005 +0200
@@ -27,9 +27,13 @@
   val context_of: state -> Proof.context
   val proof_of: state -> Proof.state
   val enter_forward_proof: state -> Proof.state
-  type transition
+  val quiet: bool ref
+  val debug: bool ref
+  val timing: bool ref
+  val profiling: int ref
   exception TERMINATE
   exception RESTART
+  type transition
   val undo_limit: bool -> int option
   val empty: transition
   val name_of: transition -> string
@@ -65,9 +69,6 @@
   val unknown_theory: transition -> transition
   val unknown_proof: transition -> transition
   val unknown_context: transition -> transition
-  val quiet: bool ref
-  val debug: bool ref
-  val profiling: int ref
   val exn_message: exn -> string
   val apply: bool -> transition -> state -> (state * (exn * string) option) option
   val excursion_result: ((transition * (state -> state -> 'a -> 'a)) list * 'a) -> 'a
@@ -180,6 +181,11 @@
 
 (** toplevel transitions **)
 
+val quiet = ref false;
+val debug = ref false;
+val timing = Output.timing;
+val profiling = ref 0;
+
 exception TERMINATE;
 exception RESTART;
 exception EXCURSION_FAIL of exn * string;
@@ -420,11 +426,6 @@
 
 (** toplevel transactions **)
 
-val quiet = ref false;
-val debug = ref false;
-val profiling = ref 0;
-
-
 (* print exceptions *)
 
 local
@@ -495,12 +496,15 @@
 
 fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state =
   let
-    val _ =
-      if int orelse not int_only then ()
-      else warning (command_msg "Interactive-only " tr);
+    val _ = conditional (not int andalso int_only) (fn () =>
+      warning (command_msg "Interactive-only " tr));
+
+    fun do_timing f x = (info (command_msg "" tr); timeap f x);
+    fun do_profiling f x = profile (! profiling) f x;
+
     val (result, opt_exn) =
-      (if ! Output.timing andalso not no_timing then (info (command_msg "" tr); timeap) else I)
-        (profile (! profiling) (apply_trans int trans)) state;
+      (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I)
+        ((if ! profiling > 0 then do_profiling else I) (apply_trans int trans)) state;
     val _ = conditional (int andalso not (! quiet) andalso
         exists (fn m => m mem_string print) ("" :: ! print_mode))
       (fn () => print_state false result);

--- a/src/Pure/drule.ML	Mon Jul 04 17:07:15 2005 +0200
+++ b/src/Pure/drule.ML	Mon Jul 04 17:08:19 2005 +0200
@@ -155,24 +155,23 @@
 struct
 
 
-(** some cterm->cterm operations: much faster than calling cterm_of! **)
+(** some cterm->cterm operations: faster than calling cterm_of! **)
 
-(** SAME NAMES as in structure Logic: use compound identifiers! **)
+(* FIXME exception CTERM (!?) *)
 
-(*dest_implies for cterms. Note T=prop below*)
 fun dest_implies ct =
-    case term_of ct of
-        (Const("==>", _) $ _ $ _) =>
-            let val (ct1,ct2) = Thm.dest_comb ct
-            in  (#2 (Thm.dest_comb ct1), ct2)  end
-      | _ => raise TERM ("dest_implies", [term_of ct]) ;
+  (case Thm.term_of ct of
+    (Const ("==>", _) $ _ $ _) =>
+      let val (ct1, ct2) = Thm.dest_comb ct
+      in (#2 (Thm.dest_comb ct1), ct2) end
+  | _ => raise TERM ("dest_implies", [term_of ct]));
 
 fun dest_equals ct =
-    case term_of ct of
-        (Const("==", _) $ _ $ _) =>
-            let val (ct1,ct2) = Thm.dest_comb ct
-            in  (#2 (Thm.dest_comb ct1), ct2)  end
-      | _ => raise TERM ("dest_equals", [term_of ct]) ;
+  (case Thm.term_of ct of
+    (Const ("==", _) $ _ $ _) =>
+      let val (ct1, ct2) = Thm.dest_comb ct
+      in (#2 (Thm.dest_comb ct1), ct2) end
+    | _ => raise TERM ("dest_equals", [term_of ct]));
 
 
 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
@@ -729,7 +728,7 @@
   let val p as (ct1, ct2) = Thm.dest_comb ct
   in (case pairself term_of p of
       (Const ("all", _), Abs (s, _, _)) =>
-         let val (v, ct') = Thm.dest_abs (SOME "@") ct2;
+         let val (v, ct') = Thm.dest_abs (SOME (gensym "all_")) ct2;
          in Thm.combination (Thm.reflexive ct1)
            (Thm.abstract_rule s v (forall_conv cv ct'))
          end