Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Sign.name_of;
authorwenzelm
Thu, 23 Oct 1997 12:48:48 +0200
changeset 3979 dac05c9341f4
parent 3978 7e1cfed19d94
child 3980 21ef91734970
Sign.name_of;
src/HOL/datatype.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle