# HG changeset patch
# User paulson
# Date 907576303 -7200
# Node ID 0e8b45a7d10470c5ee1b1b3bf12787d29f05f9ce
# Parent  5cb6129566e755ffeb75d8659dce62a27acd214f
Now prove_goalw_cterm never prints timing statistics

diff -r 5cb6129566e7 -r 0e8b45a7d104 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Mon Oct 05 10:30:57 1998 +0200
+++ b/src/Pure/goals.ML	Mon Oct 05 10:31:43 1998 +0200
@@ -238,16 +238,19 @@
 	       error ("The exception above was raised for\n" ^ 
 		      string_of_cterm chorn));
 
-(*Two variants: one checking the result, one not*)
-val prove_goalw_cterm         = prove_goalw_cterm_general true
-and prove_goalw_cterm_nocheck = prove_goalw_cterm_general false;
+(*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)
+and prove_goalw_cterm_nocheck rths chorn = 
+	setmp proof_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 = sign_of thy
       val chorn = read_cterm sign (agoal,propT)
-  in  prove_goalw_cterm rths chorn tacsf end
+  in  prove_goalw_cterm_general true rths chorn tacsf end
   handle ERROR => error (*from read_cterm?*)
 		("The error(s) above occurred for " ^ quote agoal);