Consts.eq_const is back again (cf. 907da436f8a9) -- required in ProofContext.transfer_syntax to prevent expensive merges of local_consts/global_consts;

--- a/src/Pure/Isar/proof_context.ML	Tue Mar 10 22:27:32 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Mar 10 22:49:56 2009 +0100
@@ -262,9 +262,11 @@
 
 fun transfer_syntax thy =
   map_syntax (LocalSyntax.rebuild thy) #>
-  map_consts (fn (local_consts, _) =>
-    let val thy_consts = Sign.consts_of thy
-    in (Consts.merge (local_consts, thy_consts), thy_consts) end);
+  map_consts (fn consts as (local_consts, global_consts) =>
+    let val thy_consts = Sign.consts_of thy in
+      if Consts.eq_consts (thy_consts, global_consts) then consts
+      else (Consts.merge (local_consts, thy_consts), thy_consts)
+    end);
 
 fun transfer thy = Context.transfer_proof thy #> transfer_syntax thy;
 

--- a/src/Pure/consts.ML	Tue Mar 10 22:27:32 2009 +0100
+++ b/src/Pure/consts.ML	Tue Mar 10 22:49:56 2009 +0100
@@ -8,6 +8,7 @@
 signature CONSTS =
 sig
   type T
+  val eq_consts: T * T -> bool
   val abbrevs_of: T -> string list -> (term * term) list
   val dest: T ->
    {constants: (typ * term option) NameSpace.table,
@@ -53,6 +54,13 @@
   constraints: typ Symtab.table,
   rev_abbrevs: (term * term) list Symtab.table};
 
+fun eq_consts
+   (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
+    Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) =
+  pointer_eq (decls1, decls2) andalso
+  pointer_eq (constraints1, constraints2) andalso
+  pointer_eq (rev_abbrevs1, rev_abbrevs2);
+
 fun make_consts (decls, constraints, rev_abbrevs) =
   Consts {decls = decls, constraints = constraints, rev_abbrevs = rev_abbrevs};