src/Pure/Isar/proof_context.ML

--- a/src/Pure/Isar/proof_context.ML	Sun Feb 12 21:34:26 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Feb 12 21:34:27 2006 +0100
@@ -182,7 +182,7 @@
   Ctxt of
    {naming: NameSpace.naming,                     (*local naming conventions*)
     syntax: LocalSyntax.T,                        (*local syntax*)
-    consts: Consts.T,                             (*const abbreviations*)
+    consts: Consts.T * Consts.T,                  (*global/local consts*)
     fixes: bool * (string * string) list,         (*fixes: !!x. _ with proof body flag*)
     assms:
       ((cterm list * export) list *               (*assumes and views: A ==> _*)
@@ -205,8 +205,9 @@
   val name = "Isar/context";
   type T = ctxt;
   fun init thy =
-    make_ctxt (NameSpace.default_naming, LocalSyntax.init thy, Sign.consts_of thy,
-      (false, []), ([], []), Vartab.empty, (NameSpace.empty_table, FactIndex.empty), [],
+    make_ctxt (NameSpace.default_naming, LocalSyntax.init thy,
+      (Sign.consts_of thy, Sign.consts_of thy), (false, []), ([], []),
+      Vartab.empty, (NameSpace.empty_table, FactIndex.empty), [],
       (Vartab.empty, Vartab.empty, [], Symtab.empty));
   fun print _ _ = ();
 );
@@ -260,7 +261,7 @@
 val syntax_of = #syntax o rep_context;
 val syn_of = LocalSyntax.syn_of o syntax_of;
 
-val consts_of = #consts o rep_context;
+val consts_of = #2 o #consts o rep_context;
 
 val is_body = #1 o #fixes o rep_context;
 fun set_body b = map_fixes (fn (_, fixes) => (b, fixes));
@@ -291,7 +292,11 @@
 
 fun transfer_syntax thy =
   map_syntax (LocalSyntax.rebuild thy) #>
-  map_consts (fn consts => Consts.merge (Sign.consts_of thy, consts));
+  map_consts (fn consts as (global_consts, local_consts) =>
+    let val thy_consts = Sign.consts_of thy in
+      if Consts.eq_consts (thy_consts, global_consts) then consts
+      else (thy_consts, Consts.merge (thy_consts, local_consts))
+    end);
 
 fun transfer thy = Context.transfer_proof thy #> transfer_syntax thy;
 
@@ -577,8 +582,8 @@
     | _ => I);
 
 val ins_sorts = fold_types (fold_atyps
-  (fn TFree (x, S) => Vartab.update ((x, ~1), S)
-    | TVar v => Vartab.update v
+  (fn TFree (x, S) => Vartab.replace (op =) ((x, ~1), S)
+    | TVar v => Vartab.replace (op =) v
     | _ => I));
 
 val ins_used = fold_term_types (fn t =>
@@ -1080,7 +1085,7 @@
   in
     ctxt
     |> declare_term t
-    |> map_consts (Consts.abbreviate (pp ctxt) (tsig_of ctxt) naming revert (c, t))
+    |> map_consts (apsnd (Consts.abbreviate (pp ctxt) (tsig_of ctxt) naming revert (c, t)))
     |> map_syntax (LocalSyntax.add_syntax thy [(false, (NameSpace.full naming c, T, mx))])
   end);
 
@@ -1330,8 +1335,8 @@
 
 fun pretty_consts ctxt =
   let
-    val (space, consts) = #constants (Consts.dest (consts_of ctxt));
-    val globals = #2 (#constants (Consts.dest (Sign.consts_of (theory_of ctxt))));
+    val ((_, globals), (space, consts)) =
+      pairself (#constants o Consts.dest) (#consts (rep_context ctxt));
     fun local_abbrev (_, (_, NONE)) = I
       | local_abbrev (c, (T, SOME t)) =
           if Symtab.defined globals c then I else cons (c, Logic.mk_equals (Const (c, T), t));