src/Provers/Arith/fast_lin_arith.ML

 
 fun trace_thm msg th =
   (if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th);
 
 fun trace_term ctxt msg t =
-  (if !trace then tracing (cat_lines [msg, ProofContext.string_of_term ctxt t]) else (); t)
+  (if !trace then tracing (cat_lines [msg, Syntax.string_of_term ctxt t]) else (); t)
 
 fun trace_msg msg =
   if !trace then tracing msg else ();
 
 (* FIXME OPTIMIZE!!!! (partly done already)

   case hist of
     [] => ()
   | (v, lineqs) :: hist' =>
       let
         val frees = map Free params
-        fun show_term t = ProofContext.string_of_term ctxt (subst_bounds (frees, t))
+        fun show_term t = Syntax.string_of_term ctxt (subst_bounds (frees, t))
         val start =
           if v = ~1 then (hist', findex0 discr n lineqs)
           else (hist, replicate n Rat.zero)
         val ex = SOME (produce_ex (map show_term atoms ~~ discr)
             (uncurry (fold (findex1 discr)) start))