# HG changeset patch
# User wenzelm
# Date 878307306 -3600
# Node ID 6b72919c9b4bb4d636877195b194bf755f5df415
# Parent  543df9687d7b04e3361f6a688af1f59cba188f8d
added str_of_sg: sg -> string;
improved error handling of data access;

diff -r 543df9687d7b -r 6b72919c9b4b src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Oct 30 17:05:20 1997 +0100
+++ b/src/Pure/sign.ML	Fri Oct 31 15:15:06 1997 +0100
@@ -60,6 +60,7 @@
   val intern_tycons: sg -> xtyp -> typ
   val print_sg: sg -> unit
   val pretty_sg: sg -> Pretty.T
+  val str_of_sg: sg -> string
   val pprint_sg: sg -> pprint_args -> unit
   val pretty_term: sg -> term -> Pretty.T
   val pretty_typ: sg -> typ -> Pretty.T
@@ -159,8 +160,6 @@
 val pprint_sg = Pretty.pprint o pretty_sg;
 
 val tsig_of = #tsig o rep_sg;
-val get_data = Data.get o #data o rep_sg;
-val print_data = Data.print o #data o rep_sg;
 
 fun const_type (Sg (_, {const_tab, ...})) c = Symtab.lookup (const_tab, c);
 val classes = #classes o Type.rep_tsig o tsig_of;
@@ -170,6 +169,15 @@
 val nonempty_sort = Type.nonempty_sort o tsig_of;
 
 
+(* data *)
+
+fun access_data f sg = f (#data (rep_sg sg))
+  handle ERROR => error ("of theory " ^ str_of_sg sg);
+
+val get_data = access_data Data.get;
+val print_data = access_data Data.print;
+
+
 (* id and self *)
 
 fun check_stale (sg as Sg ({id, ...},
@@ -849,7 +857,6 @@
   | merge_refs _ = sys_error "Sign.merge_refs";
 
 
-
 (* proper merge *)
 
 fun merge_aux (sg1, sg2) =