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