# HG changeset patch
# User wenzelm
# Date 877603728 -7200
# Node ID dac05c9341f4b4c488c9accd3f4fa401ece81e66
# Parent  7e1cfed19d946a79b0b352c78ec68843212c2428
Sign.name_of;

diff -r 7e1cfed19d94 -r dac05c9341f4 src/HOL/datatype.ML
--- a/src/HOL/datatype.ML	Thu Oct 23 12:47:59 1997 +0200
+++ b/src/HOL/datatype.ML	Thu Oct 23 12:48:48 1997 +0200
@@ -10,7 +10,7 @@
 
 (* Retrieve information for a specific datatype *)
 fun datatype_info thy tname =
-  case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of
+  case get_thydata (Sign.name_of (sign_of thy)) "datatypes" of
       None => None
     | Some (DT_DATA ds) => assoc (ds, tname);
 
@@ -31,7 +31,7 @@
    ancestors *)
 fun extract_info thy =
   let val (congs, rewrites) =
-        case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of
+        case get_thydata (Sign.name_of (sign_of thy)) "datatypes" of
             None => ([], [])
           | Some (DT_DATA ds) =>
               let val info = map snd ds
@@ -50,7 +50,7 @@
   end;
 
 fun get_dt_info sign tn =
-      case get_thydata (thyname_of_sign sign) "datatypes" of
+      case get_thydata (Sign.name_of sign) "datatypes" of
         None => error ("No such datatype: " ^ quote tn)
       | Some (DT_DATA ds) =>
           case assoc (ds, tn) of