proper exhaustive match (cf. e9beabf045ab);
--- a/src/Pure/Isar/args.ML Tue Aug 20 20:29:38 2013 +0200
+++ b/src/Pure/Isar/args.ML Tue Aug 20 21:17:39 2013 +0200
@@ -101,7 +101,8 @@
| Token.Typ T => Token.Typ (Morphism.typ phi T)
| Token.Term t => Token.Term (Morphism.term phi t)
| Token.Fact ths => Token.Fact (Morphism.fact phi ths)
- | Token.Attribute att => Token.Attribute (Morphism.transform phi att)));
+ | Token.Attribute att => Token.Attribute (Morphism.transform phi att)
+ | tok as Token.Files _ => tok));
val assignable = map_args Token.assignable;
val closure = map_args Token.closure;