src/Pure/consts.ML
changeset 20734 8aa9590bd452
parent 20667 953b68f4a9f3
child 21181 13c3fdccdf0d
     1.1 --- a/src/Pure/consts.ML	Wed Sep 27 20:39:09 2006 +0200
     1.2 +++ b/src/Pure/consts.ML	Wed Sep 27 21:13:09 2006 +0200
     1.3 @@ -24,8 +24,6 @@
     1.4    val syntax: T -> string * mixfix -> string * typ * mixfix
     1.5    val read_const: T -> string -> term
     1.6    val certify: Pretty.pp -> Type.tsig -> T -> term -> term          (*exception TYPE*)
     1.7 -  val serial_of: T -> string -> serial
     1.8 -  val name_of: T -> serial -> string
     1.9    val typargs: T -> string * typ -> typ list
    1.10    val instance: T -> string * typ list -> typ
    1.11    val declare: NameSpace.naming -> (bstring * typ) * bool -> T -> T
    1.12 @@ -167,19 +165,6 @@
    1.13    in cert end;
    1.14  
    1.15  
    1.16 -
    1.17 -(** efficient representations **)
    1.18 -
    1.19 -(* serial numbers *)
    1.20 -
    1.21 -fun serial_of consts c = #2 (the_const consts c);
    1.22 -
    1.23 -fun name_of (Consts ({decls = (_, tab), ...}, _)) i =
    1.24 -  (case Symtab.fold (fn (c, (_, j)) => if i = j then K (SOME c) else I) tab NONE of
    1.25 -    SOME c => c
    1.26 -  | NONE => raise TYPE ("Bad serial number of constant", [], []));
    1.27 -
    1.28 -
    1.29  (* typargs -- view actual const type as instance of declaration *)
    1.30  
    1.31  fun subscript (Type (_, Ts)) (i :: is) = subscript (nth Ts i) is