src/HOL/Tools/typedef_package.ML
changeset 17261 193b84a70ca4
parent 17144 6642e0f96f44
child 17280 a6917ddc864f
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Mon Sep 05 17:38:17 2005 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Mon Sep 05 17:38:18 2005 +0200
     1.3 @@ -62,9 +62,8 @@
     1.4  end);
     1.5  
     1.6  fun put_typedef newT oldT Abs_name Rep_name thy =
     1.7 -  TypedefData.put (Symtab.update_new
     1.8 -    ((fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name)),
     1.9 -     TypedefData.get thy)) thy;
    1.10 +  TypedefData.put (Symtab.curried_update_new
    1.11 +    (fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name)) (TypedefData.get thy)) thy;
    1.12  
    1.13  
    1.14  
    1.15 @@ -283,8 +282,10 @@
    1.16            foldl_map (Codegen.invoke_codegen thy defs dep module true) (gr', ts);
    1.17          val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'')
    1.18        in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
    1.19 -    fun lookup f T = getOpt (Option.map f (Symtab.lookup
    1.20 -      (TypedefData.get thy, get_name T)), "")
    1.21 +    fun lookup f T =
    1.22 +      (case Symtab.curried_lookup (TypedefData.get thy) (get_name T) of
    1.23 +        NONE => ""
    1.24 +      | SOME s => f s);
    1.25    in
    1.26      (case strip_comb t of
    1.27         (Const (s, Type ("fun", [T, U])), ts) =>
    1.28 @@ -303,7 +304,7 @@
    1.29    | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
    1.30  
    1.31  fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
    1.32 -      (case Symtab.lookup (TypedefData.get thy, s) of
    1.33 +      (case Symtab.curried_lookup (TypedefData.get thy) s of
    1.34           NONE => NONE
    1.35         | SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) =>
    1.36             if isSome (Codegen.get_assoc_type thy tname) then NONE else