--- 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 =
--- 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
--- 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
--- 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 *)
--- 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;
--- 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 **)