src/HOL/Complex/ex/mireif.ML

                                    | _ => error "num_of_term: unsupported Multiplication")
       | Const("RealDef.real",_)$ (Const (@{const_name "RComplete.floor"},_)$ t') => Floor (num_of_term vs t')
       | Const("RealDef.real",_)$ (Const (@{const_name "RComplete.ceiling"},_)$ t') => Neg(Floor (Neg (num_of_term vs t')))
       | Const("RealDef.real",_) $ Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
       | Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
-      | _ => error ("num_of_term: unknown term " ^ (Display.raw_string_of_term t));
+      | _ => error ("num_of_term: unknown term " ^ Sign.string_of_term CPure.thy t);
         
 
 (* pseudo reification : term -> fm *)
 fun fm_of_term vs t = 
     case t of 

       | Const("Not",_)$t' => Not (fm_of_term vs t')
       | Const("Ex",_)$Abs(xn,xT,p) => 
         E (fm_of_term (map (fn (v, n) => (v, Suc n)) vs) p)
       | Const("All",_)$Abs(xn,xT,p) => 
         A (fm_of_term (map (fn(v, n) => (v, Suc n)) vs) p)
-      | _ => error ("fm_of_term : unknown term!" ^ Display.raw_string_of_term t);
+      | _ => error ("fm_of_term : unknown term!" ^ Sign.string_of_term CPure.thy t);
 
 fun start_vs t =
     let val fs = term_frees t
     in fs ~~ map nat (0 upto  (length fs - 1))
     end ;