| changeset 61825 | 69b035408b18 |
| parent 61822 | a16497c686cb |
| child 62094 | 7d47cf67516d |
--- a/src/Pure/Isar/token.ML Thu Dec 10 13:38:40 2015 +0000 +++ b/src/Pure/Isar/token.ML Thu Dec 10 15:53:28 2015 +0100 @@ -477,7 +477,7 @@ (* src *) -fun dest_src [] = raise Fail "Empty token source" +fun dest_src ([]: src) = raise Fail "Empty token source" | dest_src (head :: args) = (head, args); fun name_of_src src =