tracing flag for arith_tac

--- a/src/HOL/Arith.ML	Thu Jun 15 16:02:12 2000 +0200
+++ b/src/HOL/Arith.ML	Fri Jun 16 13:13:55 2000 +0200
@@ -974,7 +974,8 @@
 structure Fast_Arith =
   Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref);
 
-val fast_arith_tac = Fast_Arith.lin_arith_tac;
+val fast_arith_tac = Fast_Arith.lin_arith_tac
+and trace_arith    = Fast_Arith.trace;
 
 let
 val nat_arith_simproc_pats =

--- a/src/Provers/Arith/fast_lin_arith.ML	Thu Jun 15 16:02:12 2000 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Jun 16 13:13:55 2000 +0200
@@ -17,7 +17,7 @@
 (in)equations. lin_arith_prover tries to prove or disprove the term.
 *)
 
-(* Debugging: (*? -> (*?*), !*) -> (*!*) *)
+(* Debugging: set Fast_Arith.trace *)
 
 (*** Data needed for setting up the linear arithmetic package ***)
 
@@ -73,6 +73,7 @@
 
 signature FAST_LIN_ARITH =
 sig
+  val trace           : bool ref
   val lin_arith_prover: Sign.sg -> thm list -> term -> thm option
   val     lin_arith_tac:             int -> tactic
   val cut_lin_arith_tac: thm list -> int -> tactic
@@ -89,6 +90,8 @@
    treat non-negative atoms separately rather than adding 0 <= atom
 *)
 
+val trace = ref false;
+
 datatype lineq_type = Eq | Le | Lt;
 
 datatype injust = Asm of int
@@ -194,16 +197,16 @@
         | extract xs []      = (None,xs)
   in extract [] end;
 
-(*?
 fun print_ineqs ineqs =
- writeln(cat_lines(""::map (fn Lineq(c,t,l,_) =>
-   string_of_int c ^
-   (case t of Eq => " =  " | Lt=> " <  " | Le => " <= ") ^
-   commas(map string_of_int l)) ineqs));
-!*)
+  if !trace then
+     writeln(cat_lines(""::map (fn Lineq(c,t,l,_) =>
+       string_of_int c ^
+       (case t of Eq => " =  " | Lt=> " <  " | Le => " <= ") ^
+       commas(map string_of_int l)) ineqs))
+  else ();
 
 fun elim ineqs =
-  let (*?val dummy = print_ineqs ineqs;!*)
+  let val dummy = print_ineqs ineqs;
       val (triv,nontriv) = partition is_trivial ineqs in
   if not(null triv)
   then case find_first is_answer triv of
@@ -243,6 +246,12 @@
 (* Translate back a proof.                                                   *)
 (* ------------------------------------------------------------------------- *)
 
+fun trace_thm msg th = 
+    if !trace then (writeln msg; prth th) else th;
+
+fun trace_msg msg = 
+    if !trace then writeln msg else ();
+
 (* FIXME OPTIMIZE!!!!
    Addition/Multiplication need i*t representation rather than t+t+...
 
@@ -272,16 +281,18 @@
         let val thm' = simplify (!LA_Data.ss_ref) thm
         in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end
 
-      fun mk(Asm i) = ((*?writeln"Asm";prth!*)(nth_elem(i,asms)))
-        | mk(Nat(i)) = ((*?writeln"Nat";!*)LA_Logic.mk_nat_thm sg (nth_elem(i,atoms)))
-        | mk(LessD(j)) = ((*?writeln"L";prth!*)(hd([mk j] RL !LA_Data.lessD)))
-        | mk(NotLeD(j)) = ((*?writeln"NLe";prth!*)(mk j RS LA_Logic.not_leD))
-        | mk(NotLeDD(j)) = ((*?writeln"NLeD";prth!*)(hd([mk j RS LA_Logic.not_leD] RL !LA_Data.lessD)))
-        | mk(NotLessD(j)) = ((*?writeln"NL";prth!*)(mk j RS LA_Logic.not_lessD))
-        | mk(Added(j1,j2)) = ((*?writeln"+";prth!*)(simp((*?prth!*)(addthms (mk j1) (mk j2)))))
-        | mk(Multiplied(n,j)) = ((*?writeln"*";!*)multn(n,mk j))
+      fun mk(Asm i) = trace_thm "Asm" (nth_elem(i,asms))
+        | mk(Nat(i)) = (trace_msg "Nat";
+			LA_Logic.mk_nat_thm sg (nth_elem(i,atoms)))
+        | mk(LessD(j)) = trace_thm "L" (hd([mk j] RL !LA_Data.lessD))
+        | mk(NotLeD(j)) = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
+        | mk(NotLeDD(j)) = trace_thm "NLeD" (hd([mk j RS LA_Logic.not_leD] RL 
+						!LA_Data.lessD))
+        | mk(NotLessD(j)) = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
+        | mk(Added(j1,j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2)))
+        | mk(Multiplied(n,j)) = (trace_msg "*"; multn(n,mk j))
 
-  in (*?writeln"mkthm";!*)
+  in trace_msg "mkthm";
      simplify (!LA_Data.ss_ref) (mk just) handle FalseE thm => thm end
 end;