--- a/src/HOL/Tools/recdef_package.ML Mon Sep 05 17:38:17 2005 +0200
+++ b/src/HOL/Tools/recdef_package.ML Mon Sep 05 17:38:18 2005 +0200
@@ -127,12 +127,12 @@
val print_recdefs = GlobalRecdefData.print;
-fun get_recdef thy name = Symtab.lookup (#1 (GlobalRecdefData.get thy), name);
+val get_recdef = Symtab.curried_lookup o #1 o GlobalRecdefData.get;
fun put_recdef name info thy =
let
val (tab, hints) = GlobalRecdefData.get thy;
- val tab' = Symtab.update_new ((name, info), tab)
+ val tab' = Symtab.curried_update_new (name, info) tab
handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name);
in GlobalRecdefData.put (tab', hints) thy end;