src/HOL/Tools/typedef_package.ML

   fun merge _ (tabs: T * T) = Symtab.merge (op =) tabs;
   fun print _ _ = ();
 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;
 
 
 
 (** type declarations **)
 

         val (gr', _) = Codegen.invoke_tycodegen thy defs dep module false (gr, T);
         val (gr'', ps) =
           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) =>
          if lookup #4 T = s andalso
            is_none (Codegen.get_assoc_type thy (get_name T))

 fun mk_tyexpr [] s = Pretty.str s
   | mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)]
   | 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
            let
              val module' = Codegen.if_library