# HG changeset patch
# User wenzelm
# Date 1211115864 -7200
# Node ID aec0d97a01c4f075a8a87785c12fc9c5fc56fc36
# Parent  87e4208700d1f951f58bb25f2b71efc6032c77ed
moved global pretty/string_of functions from Sign to Syntax;
removed dead code;

diff -r 87e4208700d1 -r aec0d97a01c4 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Sun May 18 15:04:22 2008 +0200
+++ b/src/HOL/Tools/record_package.ML	Sun May 18 15:04:24 2008 +0200
@@ -95,9 +95,6 @@
   let fun varify (a, S) = TVar ((a, midx + 1), S);
   in map_type_tfree varify end;
 
-fun the_plist (SOME (a,b)) = [a,b]
-  | the_plist NONE = raise Option;
-
 fun domain_type' T =
     domain_type T handle Match => T;
 
@@ -113,7 +110,7 @@
     (tracing str; map (trace_thm "") thms);
 
 fun trace_term str t =
-    tracing (str ^ Sign.string_of_term CPure.thy t);
+    tracing (str ^ Syntax.string_of_term_global CPure.thy t);
 
 (* timing *)
 
@@ -309,7 +306,7 @@
 fun print_records thy =
   let
     val {records = recs, ...} = RecordsData.get thy;
-    val prt_typ = Sign.pretty_typ thy;
+    val prt_typ = Syntax.pretty_typ_global thy;
 
     fun pretty_parent NONE = []
       | pretty_parent (SOME (Ts, name)) =