--- a/src/Pure/Isar/token.ML Wed Aug 20 16:06:10 2014 +0200
+++ b/src/Pure/Isar/token.ML Wed Aug 20 17:23:47 2014 +0200
@@ -22,6 +22,7 @@
Term of term |
Fact of string option * thm list |
Attribute of morphism -> attribute |
+ Declaration of declaration |
Files of file Exn.result list
val name0: string -> value
val pos_of: T -> Position.T
@@ -163,6 +164,7 @@
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 |
Files of file Exn.result list;
fun name0 a = Name (a, Morphism.identity);
@@ -421,6 +423,7 @@
| Term t => Term (Morphism.term phi t)
| Fact (a, ths) => Fact (a, Morphism.fact phi ths)
| Attribute att => Attribute (Morphism.transform phi att)
+ | Declaration decl => Declaration (Morphism.transform phi decl)
| Files _ => v))
and transform_src phi = map_args (transform phi);