src/HOL/Complex/ex/linrtac.ML

--- a/src/HOL/Complex/ex/linrtac.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Complex/ex/linrtac.ML	Sun May 18 15:04:09 2008 +0200
@@ -91,7 +91,7 @@
     let val pth = linr_oracle thy (Pattern.eta_long [] t1)
     in 
           (trace_msg ("calling procedure with term:\n" ^
-             Sign.string_of_term thy t1);
+             Syntax.string_of_term ctxt t1);
            ((pth RS iffD2) RS pre_thm,
             assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
     end