src/HOL/Tools/typedef_package.ML

--- a/src/HOL/Tools/typedef_package.ML	Mon Sep 05 17:38:17 2005 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Mon Sep 05 17:38:18 2005 +0200
@@ -62,9 +62,8 @@
 end);
 
 fun put_typedef newT oldT Abs_name Rep_name thy =
-  TypedefData.put (Symtab.update_new
-    ((fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name)),
-     TypedefData.get thy)) thy;
+  TypedefData.put (Symtab.curried_update_new
+    (fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name)) (TypedefData.get thy)) thy;
 
 
 
@@ -283,8 +282,10 @@
           foldl_map (Codegen.invoke_codegen thy defs dep module true) (gr', ts);
         val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'')
       in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
-    fun lookup f T = getOpt (Option.map f (Symtab.lookup
-      (TypedefData.get thy, get_name T)), "")
+    fun lookup f T =
+      (case Symtab.curried_lookup (TypedefData.get thy) (get_name T) of
+        NONE => ""
+      | SOME s => f s);
   in
     (case strip_comb t of
        (Const (s, Type ("fun", [T, U])), ts) =>
@@ -303,7 +304,7 @@
   | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
 
 fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
-      (case Symtab.lookup (TypedefData.get thy, s) of
+      (case Symtab.curried_lookup (TypedefData.get thy) s of
          NONE => NONE
        | SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) =>
            if isSome (Codegen.get_assoc_type thy tname) then NONE else