Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/isar_thy.ML
changeset 8897 fb1436ca3b2e
parent 8885 19ab913a6a6a
child 8966 916966f68907 
--- a/src/Pure/Isar/isar_thy.ML	Sun May 21 14:33:46 2000 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Sun May 21 14:35:27 2000 +0200
@@ -28,14 +28,14 @@
   val add_classes_i: (bclass * class list) list * Comment.text  -> theory -> theory
   val add_classrel: (xclass * xclass) * Comment.text -> theory -> theory
   val add_classrel_i: (class * class) * Comment.text -> theory -> theory
-  val add_defsort: xsort * Comment.text -> theory -> theory
+  val add_defsort: string * Comment.text -> theory -> theory
   val add_defsort_i: sort * Comment.text -> theory -> theory
   val add_nonterminals: (bstring * Comment.text) list -> theory -> theory
   val add_tyabbrs: ((bstring * string list * string * mixfix) * Comment.text) list
     -> theory -> theory
   val add_tyabbrs_i: ((bstring * string list * typ * mixfix) * Comment.text) list
     -> theory -> theory
-  val add_arities: ((xstring * xsort list * xsort) * Comment.text) list -> theory -> theory
+  val add_arities: ((xstring * string list * string) * Comment.text) list -> theory -> theory
   val add_arities_i: ((string * sort list * sort) * Comment.text) list -> theory -> theory
   val add_typedecl: (bstring * string list * mixfix) * Comment.text -> theory -> theory
   val add_consts: ((bstring * string * mixfix) * Comment.text) list -> theory -> theory
isabelle