proper exhaustive match (cf. e9beabf045ab);
authorwenzelm
Tue, 20 Aug 2013 21:17:39 +0200
changeset 53112 04d8af9ff64b
parent 53111 f7f1636ee2ba
child 53113 d9ba3417cb41
proper exhaustive match (cf. e9beabf045ab);
src/Pure/Isar/args.ML
--- 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;