# HG changeset patch
# User wenzelm
# Date 1377026259 -7200
# Node ID 04d8af9ff64b7d8d2a38e4288ac03fed7ea48562
# Parent  f7f1636ee2ba416d7d18a9a725f57106d4ecc4c4
proper exhaustive match (cf. e9beabf045ab);

diff -r f7f1636ee2ba -r 04d8af9ff64b 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;