src/Pure/sign.ML
changeset 17412 e26cb20ef0cc
parent 17405 e4dc583a2d79
child 17496 26535df536ae
--- a/src/Pure/sign.ML	Thu Sep 15 17:16:55 2005 +0200
+++ b/src/Pure/sign.ML	Thu Sep 15 17:16:56 2005 +0200
@@ -285,8 +285,8 @@
 
 fun const_constraint thy c =
   let val ((_, consts), constraints) = #consts (rep_sg thy) in
-    (case Symtab.curried_lookup constraints c of
-      NONE => Option.map #1 (Symtab.curried_lookup consts c)
+    (case Symtab.lookup constraints c of
+      NONE => Option.map #1 (Symtab.lookup consts c)
     | some => some)
   end;
 
@@ -294,7 +294,7 @@
   (case const_constraint thy c of SOME T => T
   | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
 
-val const_type = Option.map #1 oo (Symtab.curried_lookup o #2 o #1 o #consts o rep_sg);
+val const_type = Option.map #1 oo (Symtab.lookup o #2 o #1 o #consts o rep_sg);
 
 fun the_const_type thy c =
   (case const_type thy c of SOME T => T
@@ -517,7 +517,7 @@
 
 fun read_tyname thy raw_c =
   let val c = intern_type thy raw_c in
-    (case Symtab.curried_lookup (#2 (#types (Type.rep_tsig (tsig_of thy)))) c of
+    (case Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of thy)))) c of
       SOME (Type.LogicalType n, _) => Type (c, replicate n dummyT)
     | _ => error ("Undeclared type constructor: " ^ quote c))
   end;
@@ -717,7 +717,7 @@
       handle TYPE (msg, _, _) => error msg;
     val _ = cert_term thy (Const (c, T))
       handle TYPE (msg, _, _) => error msg;
-  in thy |> map_consts (apsnd (Symtab.curried_update (c, T))) end;
+  in thy |> map_consts (apsnd (Symtab.update (c, T))) end;
 
 val add_const_constraint = gen_add_constraint intern_const (read_typ o no_def_sort);
 val add_const_constraint_i = gen_add_constraint (K I) certify_typ;