eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;

--- a/src/Pure/Isar/proof_context.ML	Thu Mar 05 15:25:35 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 05 15:27:07 2009 +0100
@@ -263,11 +263,9 @@
 
 fun transfer_syntax thy =
   map_syntax (LocalSyntax.rebuild thy) #>
-  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);
+  map_consts (fn (local_consts, _) =>
+    let val thy_consts = Sign.consts_of thy
+    in (Consts.merge (local_consts, thy_consts), thy_consts) end);
 
 fun transfer thy = Context.transfer_proof thy #> transfer_syntax thy;
 

--- a/src/Pure/consts.ML	Thu Mar 05 15:25:35 2009 +0100
+++ b/src/Pure/consts.ML	Thu Mar 05 15:27:07 2009 +0100
@@ -8,7 +8,6 @@
 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,
@@ -52,23 +51,21 @@
 datatype T = Consts of
  {decls: ((decl * abbrev option) * serial) NameSpace.table,
   constraints: typ Symtab.table,
-  rev_abbrevs: (term * term) list Symtab.table} * stamp;
-
-fun eq_consts (Consts (_, s1), Consts (_, s2)) = s1 = s2;
+  rev_abbrevs: (term * term) list Symtab.table};
 
 fun make_consts (decls, constraints, rev_abbrevs) =
-  Consts ({decls = decls, constraints = constraints, rev_abbrevs = rev_abbrevs}, stamp ());
+  Consts {decls = decls, constraints = constraints, rev_abbrevs = rev_abbrevs};
 
-fun map_consts f (Consts ({decls, constraints, rev_abbrevs}, _)) =
+fun map_consts f (Consts {decls, constraints, rev_abbrevs}) =
   make_consts (f (decls, constraints, rev_abbrevs));
 
-fun abbrevs_of (Consts ({rev_abbrevs, ...}, _)) modes =
+fun abbrevs_of (Consts {rev_abbrevs, ...}) modes =
   maps (Symtab.lookup_list rev_abbrevs) modes;
 
 
 (* dest consts *)
 
-fun dest (Consts ({decls = (space, decls), constraints, ...}, _)) =
+fun dest (Consts {decls = (space, decls), constraints, ...}) =
  {constants = (space,
     Symtab.fold (fn (c, (({T, ...}, abbr), _)) =>
       Symtab.update (c, (T, Option.map #rhs abbr))) decls Symtab.empty),
@@ -77,7 +74,7 @@
 
 (* lookup consts *)
 
-fun the_const (Consts ({decls = (_, tab), ...}, _)) c =
+fun the_const (Consts {decls = (_, tab), ...}) c =
   (case Symtab.lookup tab c of
     SOME (decl, _) => decl
   | NONE => raise TYPE ("Unknown constant: " ^ quote c, [], []));
@@ -99,7 +96,7 @@
 
 val is_monomorphic = null oo type_arguments;
 
-fun the_constraint (consts as Consts ({constraints, ...}, _)) c =
+fun the_constraint (consts as Consts {constraints, ...}) c =
   (case Symtab.lookup constraints c of
     SOME T => T
   | NONE => type_scheme consts c);
@@ -107,7 +104,7 @@
 
 (* name space and syntax *)
 
-fun space_of (Consts ({decls = (space, _), ...}, _)) = space;
+fun space_of (Consts {decls = (space, _), ...}) = space;
 
 val intern = NameSpace.intern o space_of;
 val extern = NameSpace.extern o space_of;
@@ -307,8 +304,8 @@
 val empty = make_consts (NameSpace.empty_table, Symtab.empty, Symtab.empty);
 
 fun merge
-   (Consts ({decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1}, _),
-    Consts ({decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}, _)) =
+   (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
+    Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) =
   let
     val decls' = NameSpace.merge_tables (eq_snd (op =)) (decls1, decls2)
       handle Symtab.DUP c => err_dup_const c;