# HG changeset patch
# User wenzelm
# Date 1206625267 -3600
# Node ID 8408edac8f6bf7fee0d2a82d8e9231fc7ecb1c18
# Parent  d5883907c5147cff68374d3ebd554acb65294df6
removed Display.raw_string_of_XXX (use regular Sign.string_of_XXX);

diff -r d5883907c514 -r 8408edac8f6b src/HOL/Complex/ex/linreif.ML
--- a/src/HOL/Complex/ex/linreif.ML	Thu Mar 27 14:41:06 2008 +0100
+++ b/src/HOL/Complex/ex/linreif.ML	Thu Mar 27 14:41:07 2008 +0100
@@ -35,7 +35,7 @@
         | _ => error "num_of_term: unsupported Multiplication")
       | 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 = 
@@ -56,7 +56,7 @@
 	E(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
       | Const("All",_)$Term.Abs(xn,xT,p) => 
 	A(fm_of_term (map (fn(v,n) => (v,1+ 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 =
diff -r d5883907c514 -r 8408edac8f6b src/HOL/Complex/ex/mireif.ML
--- a/src/HOL/Complex/ex/mireif.ML	Thu Mar 27 14:41:06 2008 +0100
+++ b/src/HOL/Complex/ex/mireif.ML	Thu Mar 27 14:41:07 2008 +0100
@@ -34,7 +34,7 @@
       | 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 *)
@@ -58,7 +58,7 @@
         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
diff -r d5883907c514 -r 8408edac8f6b src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Thu Mar 27 14:41:06 2008 +0100
+++ b/src/HOL/Tools/metis_tools.ML	Thu Mar 27 14:41:07 2008 +0100
@@ -165,9 +165,10 @@
   fun apply_list rator nargs rands =
     let val trands = terms_of rands
     in  if length trands = nargs then Term (list_comb(rator, trands))
-        else error ("apply_list: wrong number of arguments: " ^ Display.raw_string_of_term rator ^
-                    " expected " ^
-                    Int.toString nargs ^ " received " ^ commas (map Display.raw_string_of_term trands))
+        else error
+          ("apply_list: wrong number of arguments: " ^ Sign.string_of_term CPure.thy rator ^
+            " expected " ^
+            Int.toString nargs ^ " received " ^ commas (map (Sign.string_of_term CPure.thy) trands))
     end;
 
 (*Instantiate constant c with the supplied types, but if they don't match its declared
diff -r d5883907c514 -r 8408edac8f6b src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Thu Mar 27 14:41:06 2008 +0100
+++ b/src/HOL/Tools/record_package.ML	Thu Mar 27 14:41:07 2008 +0100
@@ -117,7 +117,7 @@
     (tracing str; map (trace_thm "") thms);
 
 fun trace_term str t =
-    tracing (str ^ (Display.raw_string_of_term t));
+    tracing (str ^ Sign.string_of_term CPure.thy t);
 
 (* timing *)
 
diff -r d5883907c514 -r 8408edac8f6b src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Thu Mar 27 14:41:06 2008 +0100
+++ b/src/HOL/Tools/refute.ML	Thu Mar 27 14:41:07 2008 +0100
@@ -456,7 +456,7 @@
           (* schematic type variable not instantiated *)
           raise REFUTE ("monomorphic_term",
             "no substitution for type variable " ^ fst (fst v) ^
-            " in term " ^ Display.raw_string_of_term t)
+            " in term " ^ Sign.string_of_term CPure.thy t)
         | SOME typ =>
           typ)) t;
 
diff -r d5883907c514 -r 8408edac8f6b src/Pure/display.ML
--- a/src/Pure/display.ML	Thu Mar 27 14:41:06 2008 +0100
+++ b/src/Pure/display.ML	Thu Mar 27 14:41:07 2008 +0100
@@ -28,9 +28,6 @@
 signature DISPLAY =
 sig
   include BASIC_DISPLAY
-  val raw_string_of_sort: sort -> string
-  val raw_string_of_typ: typ -> string
-  val raw_string_of_term: term -> string
   val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
   val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
   val pretty_thm: thm -> Pretty.T
@@ -48,13 +45,6 @@
 structure Display: DISPLAY =
 struct
 
-(** raw output **)
-
-val raw_string_of_sort = Sign.string_of_sort ProtoPure.thy;
-val raw_string_of_typ = Sign.string_of_typ ProtoPure.thy;
-val raw_string_of_term = Sign.string_of_term ProtoPure.thy;
-
-
 
 (** print thm **)