--- a/src/Pure/Isar/isar_output.ML Thu Sep 15 17:16:55 2005 +0200
+++ b/src/Pure/Isar/isar_output.ML Thu Sep 15 17:16:56 2005 +0200
@@ -59,7 +59,7 @@
fun add_item kind (name, x) tab =
(if not (Symtab.defined tab name) then ()
else warning ("Redefined antiquotation " ^ kind ^ ": " ^ quote name);
- Symtab.curried_update (name, x) tab);
+ Symtab.update (name, x) tab);
in
@@ -68,13 +68,13 @@
fun command src =
let val ((name, _), pos) = Args.dest_src src in
- (case Symtab.curried_lookup (! global_commands) name of
+ (case Symtab.lookup (! global_commands) name of
NONE => error ("Unknown antiquotation command: " ^ quote name ^ Position.str_of pos)
| SOME f => transform_failure (curry Antiquote.ANTIQUOTE_FAIL (name, pos)) (f src))
end;
fun option (name, s) f () =
- (case Symtab.curried_lookup (! global_options) name of
+ (case Symtab.lookup (! global_options) name of
NONE => error ("Unknown antiquotation option: " ^ quote name)
| SOME opt => opt s f ());