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/token.ML
changeset 78072 001739cb8d08
parent 78064 4e865c45458b
child 78075 15ab73949713 
--- a/src/Pure/Isar/token.ML	Thu May 18 15:34:01 2023 +0200
+++ b/src/Pure/Isar/token.ML	Thu May 18 17:21:29 2023 +0200
@@ -29,8 +29,8 @@
     Typ of typ |
     Term of term |
     Fact of string option * thm list |
-    Attribute of morphism -> attribute |
-    Declaration of declaration |
+    Attribute of attribute Morphism.entity |
+    Declaration of Morphism.declaration |
     Files of file Exn.result list |
     Output of XML.body option
   val pos_of: T -> Position.T
@@ -197,8 +197,8 @@
   Typ of typ |
   Term of term |
   Fact of string option * thm list |  (*optional name for dynamic fact, i.e. fact "variable"*)
-  Attribute of morphism -> attribute |
-  Declaration of declaration |
+  Attribute of attribute Morphism.entity |
+  Declaration of Morphism.declaration |
   Files of file Exn.result list |
   Output of XML.body option;
isabelle