src/HOL/datatype.ML

 
 (** Information about datatypes **)
 
 (* 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);
 
 fun match_info thy tname =
   case datatype_info thy tname of

 
 (* Retrieve information for all datatypes defined in a theory and its
    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
               in (map #case_cong info, flat (map #case_rewrites info)) end;
   in {case_congs = congs, case_rewrites = rewrites} end;

      | Some(Type(tn,_)) => tn
      | _ => error("Cannot induct on type of " ^ quote var)
   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
             Some info => info
           | None => error ("Not a datatype: " ^ quote tn)