removed Display.raw_string_of_XXX (use regular Sign.string_of_XXX);
authorwenzelm
Thu Mar 27 14:41:07 2008 +0100 (2008-03-27)
changeset 264238408edac8f6b
parent 26422 d5883907c514
child 26424 a6cad32a27b0
removed Display.raw_string_of_XXX (use regular Sign.string_of_XXX);
src/HOL/Complex/ex/linreif.ML
src/HOL/Complex/ex/mireif.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/refute.ML
src/Pure/display.ML
     1.1 --- a/src/HOL/Complex/ex/linreif.ML	Thu Mar 27 14:41:06 2008 +0100
     1.2 +++ b/src/HOL/Complex/ex/linreif.ML	Thu Mar 27 14:41:07 2008 +0100
     1.3 @@ -35,7 +35,7 @@
     1.4          | _ => error "num_of_term: unsupported Multiplication")
     1.5        | Const("RealDef.real",_) $ Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
     1.6        | Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
     1.7 -      | _ => error ("num_of_term: unknown term " ^ (Display.raw_string_of_term t));
     1.8 +      | _ => error ("num_of_term: unknown term " ^ Sign.string_of_term CPure.thy t);
     1.9  
    1.10  (* pseudo reification : term -> fm *)
    1.11  fun fm_of_term vs t = 
    1.12 @@ -56,7 +56,7 @@
    1.13  	E(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
    1.14        | Const("All",_)$Term.Abs(xn,xT,p) => 
    1.15  	A(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
    1.16 -      | _ => error ("fm_of_term : unknown term!" ^ (Display.raw_string_of_term t));
    1.17 +      | _ => error ("fm_of_term : unknown term!" ^ Sign.string_of_term CPure.thy t);
    1.18  
    1.19  
    1.20  fun start_vs t =
     2.1 --- a/src/HOL/Complex/ex/mireif.ML	Thu Mar 27 14:41:06 2008 +0100
     2.2 +++ b/src/HOL/Complex/ex/mireif.ML	Thu Mar 27 14:41:07 2008 +0100
     2.3 @@ -34,7 +34,7 @@
     2.4        | Const("RealDef.real",_)$ (Const (@{const_name "RComplete.ceiling"},_)$ t') => Neg(Floor (Neg (num_of_term vs t')))
     2.5        | Const("RealDef.real",_) $ Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
     2.6        | Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
     2.7 -      | _ => error ("num_of_term: unknown term " ^ (Display.raw_string_of_term t));
     2.8 +      | _ => error ("num_of_term: unknown term " ^ Sign.string_of_term CPure.thy t);
     2.9          
    2.10  
    2.11  (* pseudo reification : term -> fm *)
    2.12 @@ -58,7 +58,7 @@
    2.13          E (fm_of_term (map (fn (v, n) => (v, Suc n)) vs) p)
    2.14        | Const("All",_)$Abs(xn,xT,p) => 
    2.15          A (fm_of_term (map (fn(v, n) => (v, Suc n)) vs) p)
    2.16 -      | _ => error ("fm_of_term : unknown term!" ^ Display.raw_string_of_term t);
    2.17 +      | _ => error ("fm_of_term : unknown term!" ^ Sign.string_of_term CPure.thy t);
    2.18  
    2.19  fun start_vs t =
    2.20      let val fs = term_frees t
     3.1 --- a/src/HOL/Tools/metis_tools.ML	Thu Mar 27 14:41:06 2008 +0100
     3.2 +++ b/src/HOL/Tools/metis_tools.ML	Thu Mar 27 14:41:07 2008 +0100
     3.3 @@ -165,9 +165,10 @@
     3.4    fun apply_list rator nargs rands =
     3.5      let val trands = terms_of rands
     3.6      in  if length trands = nargs then Term (list_comb(rator, trands))
     3.7 -        else error ("apply_list: wrong number of arguments: " ^ Display.raw_string_of_term rator ^
     3.8 -                    " expected " ^
     3.9 -                    Int.toString nargs ^ " received " ^ commas (map Display.raw_string_of_term trands))
    3.10 +        else error
    3.11 +          ("apply_list: wrong number of arguments: " ^ Sign.string_of_term CPure.thy rator ^
    3.12 +            " expected " ^
    3.13 +            Int.toString nargs ^ " received " ^ commas (map (Sign.string_of_term CPure.thy) trands))
    3.14      end;
    3.15  
    3.16  (*Instantiate constant c with the supplied types, but if they don't match its declared
     4.1 --- a/src/HOL/Tools/record_package.ML	Thu Mar 27 14:41:06 2008 +0100
     4.2 +++ b/src/HOL/Tools/record_package.ML	Thu Mar 27 14:41:07 2008 +0100
     4.3 @@ -117,7 +117,7 @@
     4.4      (tracing str; map (trace_thm "") thms);
     4.5  
     4.6  fun trace_term str t =
     4.7 -    tracing (str ^ (Display.raw_string_of_term t));
     4.8 +    tracing (str ^ Sign.string_of_term CPure.thy t);
     4.9  
    4.10  (* timing *)
    4.11  
     5.1 --- a/src/HOL/Tools/refute.ML	Thu Mar 27 14:41:06 2008 +0100
     5.2 +++ b/src/HOL/Tools/refute.ML	Thu Mar 27 14:41:07 2008 +0100
     5.3 @@ -456,7 +456,7 @@
     5.4            (* schematic type variable not instantiated *)
     5.5            raise REFUTE ("monomorphic_term",
     5.6              "no substitution for type variable " ^ fst (fst v) ^
     5.7 -            " in term " ^ Display.raw_string_of_term t)
     5.8 +            " in term " ^ Sign.string_of_term CPure.thy t)
     5.9          | SOME typ =>
    5.10            typ)) t;
    5.11  
     6.1 --- a/src/Pure/display.ML	Thu Mar 27 14:41:06 2008 +0100
     6.2 +++ b/src/Pure/display.ML	Thu Mar 27 14:41:07 2008 +0100
     6.3 @@ -28,9 +28,6 @@
     6.4  signature DISPLAY =
     6.5  sig
     6.6    include BASIC_DISPLAY
     6.7 -  val raw_string_of_sort: sort -> string
     6.8 -  val raw_string_of_typ: typ -> string
     6.9 -  val raw_string_of_term: term -> string
    6.10    val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
    6.11    val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
    6.12    val pretty_thm: thm -> Pretty.T
    6.13 @@ -48,13 +45,6 @@
    6.14  structure Display: DISPLAY =
    6.15  struct
    6.16  
    6.17 -(** raw output **)
    6.18 -
    6.19 -val raw_string_of_sort = Sign.string_of_sort ProtoPure.thy;
    6.20 -val raw_string_of_typ = Sign.string_of_typ ProtoPure.thy;
    6.21 -val raw_string_of_term = Sign.string_of_term ProtoPure.thy;
    6.22 -
    6.23 -
    6.24  
    6.25  (** print thm **)
    6.26