src/Pure/sign.ML
changeset 17412 e26cb20ef0cc
parent 17405 e4dc583a2d79
child 17496 26535df536ae
     1.1 --- a/src/Pure/sign.ML	Thu Sep 15 17:16:55 2005 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Sep 15 17:16:56 2005 +0200
     1.3 @@ -285,8 +285,8 @@
     1.4  
     1.5  fun const_constraint thy c =
     1.6    let val ((_, consts), constraints) = #consts (rep_sg thy) in
     1.7 -    (case Symtab.curried_lookup constraints c of
     1.8 -      NONE => Option.map #1 (Symtab.curried_lookup consts c)
     1.9 +    (case Symtab.lookup constraints c of
    1.10 +      NONE => Option.map #1 (Symtab.lookup consts c)
    1.11      | some => some)
    1.12    end;
    1.13  
    1.14 @@ -294,7 +294,7 @@
    1.15    (case const_constraint thy c of SOME T => T
    1.16    | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
    1.17  
    1.18 -val const_type = Option.map #1 oo (Symtab.curried_lookup o #2 o #1 o #consts o rep_sg);
    1.19 +val const_type = Option.map #1 oo (Symtab.lookup o #2 o #1 o #consts o rep_sg);
    1.20  
    1.21  fun the_const_type thy c =
    1.22    (case const_type thy c of SOME T => T
    1.23 @@ -517,7 +517,7 @@
    1.24  
    1.25  fun read_tyname thy raw_c =
    1.26    let val c = intern_type thy raw_c in
    1.27 -    (case Symtab.curried_lookup (#2 (#types (Type.rep_tsig (tsig_of thy)))) c of
    1.28 +    (case Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of thy)))) c of
    1.29        SOME (Type.LogicalType n, _) => Type (c, replicate n dummyT)
    1.30      | _ => error ("Undeclared type constructor: " ^ quote c))
    1.31    end;
    1.32 @@ -717,7 +717,7 @@
    1.33        handle TYPE (msg, _, _) => error msg;
    1.34      val _ = cert_term thy (Const (c, T))
    1.35        handle TYPE (msg, _, _) => error msg;
    1.36 -  in thy |> map_consts (apsnd (Symtab.curried_update (c, T))) end;
    1.37 +  in thy |> map_consts (apsnd (Symtab.update (c, T))) end;
    1.38  
    1.39  val add_const_constraint = gen_add_constraint intern_const (read_typ o no_def_sort);
    1.40  val add_const_constraint_i = gen_add_constraint (K I) certify_typ;