--- a/src/HOL/Tools/inductive_package.ML Mon Sep 05 17:38:17 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML Mon Sep 05 17:38:18 2005 +0200
@@ -112,7 +112,7 @@
(* get and put data *)
-fun get_inductive thy name = Symtab.lookup (fst (InductiveData.get thy), name);
+val get_inductive = Symtab.curried_lookup o #1 o InductiveData.get;
fun the_inductive thy name =
(case get_inductive thy name of
@@ -123,7 +123,7 @@
fun put_inductives names info thy =
let
- fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);
+ fun upd ((tab, monos), name) = (Symtab.curried_update_new (name, info) tab, monos);
val tab_monos = Library.foldl upd (InductiveData.get thy, names)
handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
in InductiveData.put tab_monos thy end;