src/Pure/goals.ML

   val printyp		: typ -> unit
   val pprint_term	: term -> pprint_args -> unit
   val pprint_typ	: typ -> pprint_args -> unit
   val print_exn		: exn -> 'a
   val print_sign_exn	: Sign.sg -> exn -> 'a
-  val proof_timing	: bool ref
   val prove_goal	: theory -> string -> (thm list -> tactic list) -> thm
   val prove_goalw      : theory->thm list->string->(thm list->tactic list)->thm
   val prove_goalw_cterm	: thm list->cterm->(thm list->tactic list)->thm
   val prove_goalw_cterm_nocheck	: thm list->cterm->(thm list->tactic list)->thm
   val push_proof	: unit -> unit

 
 datatype proof = Proof of gstack list * thm list * (bool*thm->thm);
 
 
 (*** References ***)
-
-(*Should process time be printed after proof steps?*)
-val proof_timing = ref false;
 
 (*Current assumption list -- set by "goal".*)
 val curr_prems = ref([] : thm list);
 
 (*Return assumption list -- useful if you didn't save "goal"'s result. *)

       val tac = EVERY (tacsf prems)
       fun statef() = 
 	  (case Seq.pull (tac st0) of 
 	       Some(st,_) => st
 	     | _ => error ("prove_goal: tactic failed"))
-  in  mkresult (check, cond_timeit (!proof_timing) statef)  end
+  in  mkresult (check, cond_timeit (!Library.timing) statef)  end
   handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e;
 	       writeln ("The exception above was raised for\n" ^ 
 		      string_of_cterm chorn); raise e);
 
 (*Two variants: one checking the result, one not.  
   Neither prints runtime messages: they are for internal packages.*)
 fun prove_goalw_cterm rths chorn = 
-	setmp proof_timing false (prove_goalw_cterm_general true rths chorn)
+	setmp Library.timing false (prove_goalw_cterm_general true rths chorn)
 and prove_goalw_cterm_nocheck rths chorn = 
-	setmp proof_timing false (prove_goalw_cterm_general false rths chorn);
+	setmp Library.timing false (prove_goalw_cterm_general false rths chorn);
 
 
 (*Version taking the goal as a string*)
 fun prove_goalw thy rths agoal tacsf =
   let val sign = Theory.sign_of thy

 	  else if eq_thm_sg(th,th2) then ()
 	  else warning ("Warning: signature of proof state has changed" ^
 		       sign_error (#sign(rep_thm th), #sign(rep_thm th2)));
        ((th2,ths2)::(th,ths)::pairs)));
 
-fun by tac = cond_timeit (!proof_timing) 
+fun by tac = cond_timeit (!Library.timing) 
     (fn() => make_command (by_com tac));
 
 (* byev[tac1,...,tacn] applies tac1 THEN ... THEN tacn.
    Good for debugging proofs involving prove_goal.*)
 val byev = by o EVERY;