src/HOL/Complex/ex/linrtac.ML

     val (th, tac) = case (prop_of pre_thm) of
         Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
     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
       | _ => (pre_thm, assm_tac i)
   in (rtac (((mp_step nh) o (spec_step np)) th) i