more frugal recording of changes: join merely requires information from one side;
tuned;

--- a/src/Pure/General/change_table.ML	Thu Mar 13 15:05:56 2014 +0100
+++ b/src/Pure/General/change_table.ML	Thu Mar 13 17:26:22 2014 +0100
@@ -17,6 +17,7 @@
   val empty: 'a T
   val is_empty: 'a T -> bool
   val change_base: bool -> 'a T -> 'a T
+  val change_ignore: 'a T -> 'a T
   val join: (key -> 'a * 'a -> 'a) (*exception SAME*) -> 'a T * 'a T -> 'a T  (*exception DUP*)
   val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T  (*exception DUP*)
   val fold: (key * 'b -> 'a -> 'a) -> 'b T -> 'a -> 'a
@@ -43,35 +44,42 @@
 
 (* optional change *)
 
-datatype change = No_Change | Change of {base: serial, depth: int, changes: Table.set};
+datatype change =
+  No_Change | Change of {base: serial, depth: int, changes: Table.set option};
 
 fun make_change base depth changes =
   Change {base = base, depth = depth, changes = changes};
 
+fun ignore_change (Change {base, depth, changes = SOME _}) =
+      make_change base depth NONE
+  | ignore_change change = change;
+
+fun update_change key (Change {base, depth, changes = SOME ch}) =
+      make_change base depth (SOME (Table.insert (K true) (key, ()) ch))
+  | update_change _ change = change;
+
 fun base_change true No_Change =
-      make_change (serial ()) 0 Table.empty
+      make_change (serial ()) 0 (SOME Table.empty)
   | base_change true (Change {base, depth, changes}) =
       make_change base (depth + 1) changes
   | base_change false (Change {base, depth, changes}) =
       if depth = 0 then No_Change else make_change base (depth - 1) changes
-  | base_change false No_Change = raise Fail "Unbalanced block structure of change table";
+  | base_change false No_Change = raise Fail "Unbalanced change structure";
 
-fun update_change _ No_Change = No_Change
-  | update_change key (Change {base, depth, changes}) =
-      make_change base depth (Table.insert (K true) (key, ()) changes);
-
-fun cannot_merge () = raise Fail "Attempt to merge tables with incompatible change base";
+fun cannot_merge () = raise Fail "Cannot merge: incompatible change structure";
 
 fun merge_change (No_Change, No_Change) = NONE
   | merge_change (Change change1, Change change2) =
       let
         val {base = base1, depth = depth1, changes = changes1} = change1;
         val {base = base2, depth = depth2, changes = changes2} = change2;
-      in
-        if base1 = base2 andalso depth1 = depth2 then
-          SOME ((changes2, make_change base1 depth1 (Table.merge (K true) (changes1, changes2))))
-        else cannot_merge ()
-      end
+        val _ = if base1 = base2 andalso depth1 = depth2 then () else cannot_merge ();
+        val (swapped, ch2) =
+          (case (changes1, changes2) of
+            (_, SOME ch2) => (false, ch2)
+          | (SOME ch1, _) => (true, ch1)
+          | _ => cannot_merge ());
+      in SOME (swapped, ch2, make_change base1 depth1 NONE) end
   | merge_change _ = cannot_merge ();
 
 
@@ -90,6 +98,7 @@
 fun map_change_table f (Change_Table {change, table}) = make_change_table (f (change, table));
 
 fun change_base begin = (map_change_table o apfst) (base_change begin);
+fun change_ignore arg = (map_change_table o apfst) ignore_change arg;
 
 
 (* join and merge *)
@@ -105,20 +114,21 @@
     else
       (case merge_change (change1, change2) of
         NONE => make_change_table (No_Change, Table.join f (table1, table2))
-      | SOME (changes2, change') =>
+      | SOME (swapped, ch2, change') =>
           let
-            fun update key table =
-              (case Table.lookup table2 key of
-                NONE => table
+            fun maybe_swap (x, y) = if swapped then (y, x) else (x, y);
+            val (tab1, tab2) = maybe_swap (table1, table2);
+            fun update key tab =
+              (case Table.lookup tab2 key of
+                NONE => tab
               | SOME y =>
-                  (case Table.lookup table key of
-                    NONE => Table.update (key, y) table
+                  (case Table.lookup tab key of
+                    NONE => Table.update (key, y) tab
                   | SOME x =>
-                      (case (SOME (f key (x, y)) handle Table.SAME => NONE) of
-                        NONE => table
-                      | SOME z => Table.update (key, z) table)));
-            val table' = Table.fold (update o #1) changes2 table1;
-          in make_change_table (change', table') end)
+                      (case (SOME (f key (maybe_swap (x, y))) handle Table.SAME => NONE) of
+                        NONE => tab
+                      | SOME z => Table.update (key, z) tab)));
+          in make_change_table (change', Table.fold (update o #1) ch2 tab1) end)
   end;
 
 fun merge eq =

--- a/src/Pure/General/name_space.ML	Thu Mar 13 15:05:56 2014 +0100
+++ b/src/Pure/General/name_space.ML	Thu Mar 13 17:26:22 2014 +0100
@@ -56,6 +56,7 @@
   val declare: Context.generic -> bool -> binding -> T -> string * T
   type 'a table
   val change_base: bool -> 'a table -> 'a table
+  val change_ignore: 'a table -> 'a table
   val space_of_table: 'a table -> T
   val check_reports: Context.generic -> 'a table ->
     xstring * Position.T list -> (string * Position.report list) * 'a
@@ -123,6 +124,9 @@
 fun change_base_space begin = map_name_space (fn (kind, internals, entries) =>
   (kind, Change_Table.change_base begin internals, Change_Table.change_base begin entries));
 
+val change_ignore_space = map_name_space (fn (kind, internals, entries) =>
+  (kind, Change_Table.change_ignore internals, Change_Table.change_ignore entries));
+
 fun map_internals f xname = map_name_space (fn (kind, internals, entries) =>
   (kind, Change_Table.map_default (xname, ([], [])) f internals, entries));
 
@@ -474,6 +478,9 @@
 fun change_base begin (Table (space, tab)) =
   Table (change_base_space begin space, Change_Table.change_base begin tab);
 
+fun change_ignore (Table (space, tab)) =
+  Table (change_ignore_space space, Change_Table.change_ignore tab);
+
 fun space_of_table (Table (space, _)) = space;
 
 fun check_reports context (Table (space, tab)) (xname, ps) =

--- a/src/Pure/Isar/proof_context.ML	Thu Mar 13 15:05:56 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 13 17:26:22 2014 +0100
@@ -219,9 +219,12 @@
 (
   type T = data;
   fun init thy =
-    make_data (mode_default, Local_Syntax.init thy,
-      (Sign.tsig_of thy, Sign.tsig_of thy),
-      (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, empty_cases);
+    make_data (mode_default,
+      Local_Syntax.init thy,
+      (Type.change_ignore (Sign.tsig_of thy), Sign.tsig_of thy),
+      (Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy),
+      Facts.empty,
+      empty_cases);
 );
 
 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);

--- a/src/Pure/consts.ML	Thu Mar 13 15:05:56 2014 +0100
+++ b/src/Pure/consts.ML	Thu Mar 13 17:26:22 2014 +0100
@@ -10,6 +10,7 @@
   type T
   val eq_consts: T * T -> bool
   val change_base: bool -> T -> T
+  val change_ignore: T -> T
   val retrieve_abbrevs: T -> string list -> term -> (term * term) list
   val dest: T ->
    {const_space: Name_Space.T,
@@ -69,6 +70,9 @@
 fun change_base begin = map_consts (fn (decls, constraints, rev_abbrevs) =>
   (Name_Space.change_base begin decls, constraints, rev_abbrevs));
 
+val change_ignore = map_consts (fn (decls, constraints, rev_abbrevs) =>
+  (Name_Space.change_ignore decls, constraints, rev_abbrevs));
+
 
 (* reverted abbrevs *)
 

--- a/src/Pure/type.ML	Thu Mar 13 15:05:56 2014 +0100
+++ b/src/Pure/type.ML	Thu Mar 13 17:26:22 2014 +0100
@@ -26,6 +26,7 @@
     types: decl Name_Space.table,
     log_types: string list}
   val change_base: bool -> tsig -> tsig
+  val change_ignore: tsig -> tsig
   val empty_tsig: tsig
   val class_space: tsig -> Name_Space.T
   val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
@@ -180,6 +181,9 @@
 fun change_base begin (TSig {classes, default, types, log_types}) =
   make_tsig (classes, default, Name_Space.change_base begin types, log_types);
 
+fun change_ignore (TSig {classes, default, types, log_types}) =
+  make_tsig (classes, default, Name_Space.change_ignore types, log_types);
+
 fun build_tsig (classes, default, types) =
   let
     val log_types =