| changeset 8586 | e451c4865548 |
| parent 8581 | 5c7ed2af8bfb |
| child 8648 | 7461dc59a818 |
--- a/src/Pure/Isar/outer_parse.ML Sun Mar 26 20:17:52 2000 +0200 +++ b/src/Pure/Isar/outer_parse.ML Sun Mar 26 20:38:23 2000 +0200 @@ -96,8 +96,8 @@ | err (toks, Some msg) = kind ^ get_pos toks ^ ": " ^ msg; in Scan.!! err scan end; -val !!! = cut "Outer syntax error"; -val !!!! = cut "Corrupted outer syntax in presentation"; +fun !!! scan = cut "Outer syntax error" scan; +fun !!!! scan = cut "Corrupted outer syntax in presentation" scan;