src/Pure/consts.ML
changeset 30424 692279df7cc2
parent 30364 577edc39b501
child 30466 5f31e24937c5
     1.1 --- a/src/Pure/consts.ML	Tue Mar 10 22:27:32 2009 +0100
     1.2 +++ b/src/Pure/consts.ML	Tue Mar 10 22:49:56 2009 +0100
     1.3 @@ -8,6 +8,7 @@
     1.4  signature CONSTS =
     1.5  sig
     1.6    type T
     1.7 +  val eq_consts: T * T -> bool
     1.8    val abbrevs_of: T -> string list -> (term * term) list
     1.9    val dest: T ->
    1.10     {constants: (typ * term option) NameSpace.table,
    1.11 @@ -53,6 +54,13 @@
    1.12    constraints: typ Symtab.table,
    1.13    rev_abbrevs: (term * term) list Symtab.table};
    1.14  
    1.15 +fun eq_consts
    1.16 +   (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
    1.17 +    Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) =
    1.18 +  pointer_eq (decls1, decls2) andalso
    1.19 +  pointer_eq (constraints1, constraints2) andalso
    1.20 +  pointer_eq (rev_abbrevs1, rev_abbrevs2);
    1.21 +
    1.22  fun make_consts (decls, constraints, rev_abbrevs) =
    1.23    Consts {decls = decls, constraints = constraints, rev_abbrevs = rev_abbrevs};
    1.24