# HG changeset patch
# User wenzelm
# Date 1357668132 -3600
# Node ID 5a9964f7a6915cfa8a144fc9acc9fddec562ff9b
# Parent  26ad3da13f47c1a1d301a7c02a73fcb03aaa1f74# Parent  8c1cda8ad83306a2bca6533052a8af07b4122bdb
merged

diff -r 26ad3da13f47 -r 5a9964f7a691 NEWS
--- a/NEWS	Tue Jan 08 13:16:39 2013 +0100
+++ b/NEWS	Tue Jan 08 19:02:12 2013 +0100
@@ -38,6 +38,13 @@
 specifications: nesting of "context fixes ... context assumes ..."
 and "class ... context ...".
 
+* Attribute "consumes" allows a negative value as well, which is
+interpreted relatively to the total number if premises of the rule in
+the target context.  This form of declaration is stable when exported
+from a nested 'context' with additional assumptions.  It is the
+preferred form for definitional packages, notably cases/rules produced
+in HOL/inductive and HOL/function.
+
 * More informative error messages for Isar proof commands involving
 lazy enumerations (method applications etc.).
 
diff -r 26ad3da13f47 -r 5a9964f7a691 src/Doc/IsarRef/Proof.thy
--- a/src/Doc/IsarRef/Proof.thy	Tue Jan 08 13:16:39 2013 +0100
+++ b/src/Doc/IsarRef/Proof.thy	Tue Jan 08 19:02:12 2013 +0100
@@ -1197,7 +1197,7 @@
     ;
     @@{attribute params} ((@{syntax name} * ) + @'and')
     ;
-    @@{attribute consumes} @{syntax nat}?
+    @@{attribute consumes} @{syntax int}?
   "}
 
   \begin{description}
@@ -1245,7 +1245,15 @@
   \secref{sec:hol-inductive}).  Rules without any @{attribute
   consumes} declaration given are treated as if @{attribute
   consumes}~@{text 0} had been specified.
-  
+
+  A negative @{text n} is interpreted relatively to the total number
+  if premises of the rule in the target context.  Thus its absolute
+  value specifies the remaining number of premises, after subtracting
+  the prefix of major premises as indicated above. This form of
+  declaration has the technical advantage of being stable under more
+  morphisms, notably those that export the result from a nested
+  @{command_ref context} with additional assumptions.
+
   Note that explicit @{attribute consumes} declarations are only
   rarely needed; this is already taken care of automatically by the
   higher-level @{attribute cases}, @{attribute induct}, and
diff -r 26ad3da13f47 -r 5a9964f7a691 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Tue Jan 08 13:16:39 2013 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Tue Jan 08 19:02:12 2013 +0100
@@ -540,7 +540,7 @@
 
   in
     ctxt'' |>
-    Proof.theorem NONE (fn thss => fn ctxt =>
+    Proof.theorem NONE (fn thss => fn ctxt => (* FIXME ctxt/ctxt' should be called lthy/lthy' *)
       let
         val rec_name = space_implode "_" (map Long_Name.base_name names);
         val rec_qualified = Binding.qualify false rec_name;
@@ -553,27 +553,27 @@
           mk_ind_proof ctxt thss' |> Inductive.rulify;
         val strong_cases = map (mk_cases_proof ##> Inductive.rulify)
           (thsss ~~ elims ~~ cases_prems ~~ cases_prems');
+        val strong_induct_atts =
+          map (Attrib.internal o K)
+            [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of strong_raw_induct))];
         val strong_induct =
-          if length names > 1 then
-            (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
-          else (strong_raw_induct RSN (2, rev_mp),
-            [ind_case_names, Rule_Cases.consumes 1]);
+          if length names > 1 then strong_raw_induct
+          else strong_raw_induct RSN (2, rev_mp);
         val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note
-          ((rec_qualified (Binding.name "strong_induct"),
-            map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]);
+          ((rec_qualified (Binding.name "strong_induct"), strong_induct_atts), [strong_induct]);
         val strong_inducts =
           Project_Rule.projects ctxt (1 upto length names) strong_induct';
       in
         ctxt' |>
-        Local_Theory.note
-          ((rec_qualified (Binding.name "strong_inducts"),
-            [Attrib.internal (K ind_case_names),
-             Attrib.internal (K (Rule_Cases.consumes 1))]),
-           strong_inducts) |> snd |>
+        Local_Theory.notes
+          [((rec_qualified (Binding.name "strong_inducts"), []),
+            strong_inducts |> map (fn th => ([th],
+              [Attrib.internal (K ind_case_names),
+               Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th)))])))] |> snd |>
         Local_Theory.notes (map (fn ((name, elim), (_, cases)) =>
             ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
               [Attrib.internal (K (Rule_Cases.case_names (map snd cases))),
-               Attrib.internal (K (Rule_Cases.consumes 1))]), [([elim], [])]))
+               Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of elim)))]), [([elim], [])]))
           (strong_cases ~~ induct_cases')) |> snd
       end)
       (map (map (rulify_term thy #> rpair [])) vc_compat)
diff -r 26ad3da13f47 -r 5a9964f7a691 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Tue Jan 08 13:16:39 2013 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Tue Jan 08 19:02:12 2013 +0100
@@ -443,7 +443,7 @@
 
   in
     ctxt'' |>
-    Proof.theorem NONE (fn thss => fn ctxt =>
+    Proof.theorem NONE (fn thss => fn ctxt =>  (* FIXME ctxt/ctxt' should be called lthy/lthy' *)
       let
         val rec_name = space_implode "_" (map Long_Name.base_name names);
         val rec_qualified = Binding.qualify false rec_name;
@@ -454,28 +454,27 @@
         val thsss = Inductive.partition_rules' raw_induct (intrs ~~ thss');
         val strong_raw_induct =
           mk_ind_proof ctxt thss' |> Inductive.rulify;
+        val strong_induct_atts =
+          map (Attrib.internal o K)
+            [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of strong_raw_induct))];
         val strong_induct =
-          if length names > 1 then
-            (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
-          else (strong_raw_induct RSN (2, rev_mp),
-            [ind_case_names, Rule_Cases.consumes 1]);
+          if length names > 1 then strong_raw_induct
+          else strong_raw_induct RSN (2, rev_mp);
         val (induct_name, inducts_name) =
           case alt_name of
             NONE => (rec_qualified (Binding.name "strong_induct"),
                      rec_qualified (Binding.name "strong_inducts"))
           | SOME s => (Binding.name s, Binding.name (s ^ "s"));
         val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note
-          ((induct_name,
-            map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]);
+          ((induct_name, strong_induct_atts), [strong_induct]);
         val strong_inducts =
           Project_Rule.projects ctxt' (1 upto length names) strong_induct'
       in
         ctxt' |>
-        Local_Theory.note
-          ((inducts_name,
+        Local_Theory.notes [((inducts_name, []),
+          strong_inducts |> map (fn th => ([th],
             [Attrib.internal (K ind_case_names),
-             Attrib.internal (K (Rule_Cases.consumes 1))]),
-           strong_inducts) |> snd
+             Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th)))])))] |> snd
       end)
       (map (map (rulify_term thy #> rpair [])) vc_compat)
   end;
diff -r 26ad3da13f47 -r 5a9964f7a691 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Tue Jan 08 13:16:39 2013 +0100
+++ b/src/HOL/Tools/Function/function.ML	Tue Jan 08 19:02:12 2013 +0100
@@ -105,14 +105,15 @@
 
         val addsmps = add_simps fnames post sort_cont
 
-        val (((psimps', pinducts'), (_, [termination'])), lthy) =
+        val (((psimps', [pinducts']), (_, [termination'])), lthy) =
           lthy
           |> addsmps (conceal_partial o Binding.qualify false "partial")
                "psimps" conceal_partial psimp_attribs psimps
-          ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
+          ||>> Local_Theory.notes [((conceal_partial (qualify "pinduct"), []),
+                simple_pinducts |> map (fn th => ([th],
                  [Attrib.internal (K (Rule_Cases.case_names cnames)),
-                  Attrib.internal (K (Rule_Cases.consumes 1)),
-                  Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
+                  Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))),
+                  Attrib.internal (K (Induct.induct_pred ""))])))]
           ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])
           ||> (snd o Local_Theory.note ((qualify "cases",
                  [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
diff -r 26ad3da13f47 -r 5a9964f7a691 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue Jan 08 13:16:39 2013 +0100
+++ b/src/HOL/Tools/inductive.ML	Tue Jan 08 19:02:12 2013 +0100
@@ -860,12 +860,17 @@
     val ind_case_names = Rule_Cases.case_names intr_names;
     val induct =
       if coind then
-        (raw_induct, [Rule_Cases.case_names [rec_name],
+        (raw_induct,
+         [Rule_Cases.case_names [rec_name],
           Rule_Cases.case_conclusion (rec_name, intr_names),
-          Rule_Cases.consumes 1, Induct.coinduct_pred (hd cnames)])
+          Rule_Cases.consumes (1 - Thm.nprems_of raw_induct),
+          Induct.coinduct_pred (hd cnames)])
       else if no_ind orelse length cnames > 1 then
-        (raw_induct, [ind_case_names, Rule_Cases.consumes 0])
-      else (raw_induct RSN (2, rev_mp), [ind_case_names, Rule_Cases.consumes 1]);
+        (raw_induct,
+          [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of raw_induct))])
+      else
+        (raw_induct RSN (2, rev_mp),
+          [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of raw_induct))]);
 
     val (intrs', lthy1) =
       lthy |>
@@ -883,7 +888,7 @@
         Local_Theory.note
           ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
             [Attrib.internal (K (Rule_Cases.case_names cases)),
-             Attrib.internal (K (Rule_Cases.consumes 1)),
+             Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of elim))),
              Attrib.internal (K (Rule_Cases.constraints k)),
              Attrib.internal (K (Induct.cases_pred name)),
              Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
@@ -906,7 +911,7 @@
           Local_Theory.notes [((rec_qualified true (Binding.name "inducts"), []),
             inducts |> map (fn (name, th) => ([th],
               [Attrib.internal (K ind_case_names),
-               Attrib.internal (K (Rule_Cases.consumes 1)),
+               Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))),
                Attrib.internal (K (Induct.induct_pred name))])))] |>> snd o hd
         end;
   in (intrs', elims', eqs', induct', inducts, lthy4) end;
diff -r 26ad3da13f47 -r 5a9964f7a691 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Tue Jan 08 13:16:39 2013 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Tue Jan 08 19:02:12 2013 +0100
@@ -156,7 +156,7 @@
 (* where s and p are parameters                            *)
 (***********************************************************)
 
-structure PredSetConvData = Generic_Data
+structure Data = Generic_Data
 (
   type T =
     {(* rules for converting predicates to sets *)
@@ -269,13 +269,15 @@
 
 (**** declare rules for converting predicates to sets ****)
 
-fun add ctxt thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) =
-  case prop_of thm of
+exception Malformed of string;
+
+fun add context thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) =
+  (case prop_of thm of
     Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ lhs $ rhs) =>
       (case body_type T of
          @{typ bool} =>
            let
-             val thy = Context.theory_of ctxt;
+             val thy = Context.theory_of context;
              fun factors_of t fs = case strip_abs_body t of
                  Const (@{const_name Set.member}, _) $ u $ S =>
                    if is_Free S orelse is_Var S then
@@ -289,7 +291,7 @@
                  Abs _ => (case strip_abs_body rhs of
                      Const (@{const_name Set.member}, _) $ u $ S =>
                        (strip_comb S, SOME (HOLogic.flat_tuple_paths u))
-                   | _ => error "member symbol on right-hand side expected")
+                   | _ => raise Malformed "member symbol on right-hand side expected")
                | _ => (strip_comb rhs, NONE))
            in
              case (name_type_of h, name_type_of h') of
@@ -308,13 +310,16 @@
                       (T', (map (AList.lookup op = fs) ts', fs'))) set_arities,
                     pred_arities = Symtab.insert_list op = (s,
                       (T, (pfs, fs'))) pred_arities}
-             | _ => error "set / predicate constant expected"
+             | _ => raise Malformed "set / predicate constant expected"
            end
-       | _ => error "equation between predicates expected")
-  | _ => error "equation expected";
+       | _ => raise Malformed "equation between predicates expected")
+  | _ => raise Malformed "equation expected")
+  handle Malformed msg =>
+    (warning ("Ignoring malformed set / predicate conversion rule: " ^ msg ^
+      "\n" ^ Display.string_of_thm (Context.proof_of context) thm); tab);
 
 val pred_set_conv_att = Thm.declaration_attribute
-  (fn thm => fn ctxt => PredSetConvData.map (add ctxt thm) ctxt);
+  (fn thm => fn ctxt => Data.map (add ctxt thm) ctxt);
 
 
 (**** convert theorem in set notation to predicate notation ****)
@@ -340,7 +345,7 @@
   let
     val thy = Context.theory_of ctxt;
     val {to_pred_simps, set_arities, pred_arities, ...} =
-      fold (add ctxt) thms (PredSetConvData.get ctxt);
+      fold (add ctxt) thms (Data.get ctxt);
     val fs = filter (is_Var o fst)
       (infer_arities thy set_arities (NONE, prop_of thm) []);
     (* instantiate each set parameter with {(x, y). p x y} *)
@@ -363,7 +368,7 @@
   let
     val thy = Context.theory_of ctxt;
     val {to_set_simps, pred_arities, ...} =
-      fold (add ctxt) thms (PredSetConvData.get ctxt);
+      fold (add ctxt) thms (Data.get ctxt);
     val fs = filter (is_Var o fst)
       (infer_arities thy pred_arities (NONE, prop_of thm) []);
     (* instantiate each predicate parameter with %x y. (x, y) : s *)
@@ -397,7 +402,7 @@
 fun codegen_preproc thy =
   let
     val {to_pred_simps, set_arities, pred_arities, ...} =
-      PredSetConvData.get (Context.Theory thy);
+      Data.get (Context.Theory thy);
     fun preproc thm =
       if exists_Const (fn (s, _) => case Symtab.lookup set_arities s of
           NONE => false
@@ -422,7 +427,7 @@
   let
     val thy = Proof_Context.theory_of lthy;
     val {set_arities, pred_arities, to_pred_simps, ...} =
-      PredSetConvData.get (Context.Proof lthy);
+      Data.get (Context.Proof lthy);
     fun infer (Abs (_, _, t)) = infer t
       | infer (Const (@{const_name Set.member}, _) $ t $ u) =
           infer_arities thy set_arities (SOME (HOLogic.flat_tuple_paths t), u)
diff -r 26ad3da13f47 -r 5a9964f7a691 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Jan 08 13:16:39 2013 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Jan 08 19:02:12 2013 +0100
@@ -391,7 +391,7 @@
     "rename bound variables in abstractions" #>
   setup (Binding.name "unfolded") unfolded "unfolded definitions" #>
   setup (Binding.name "folded") folded "folded definitions" #>
-  setup (Binding.name "consumes") (Scan.lift (Scan.optional Parse.nat 1) >> Rule_Cases.consumes)
+  setup (Binding.name "consumes") (Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes)
     "number of consumed facts" #>
   setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
     "number of equality constraints" #>
diff -r 26ad3da13f47 -r 5a9964f7a691 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Jan 08 13:16:39 2013 +0100
+++ b/src/Pure/axclass.ML	Tue Jan 08 19:02:12 2013 +0100
@@ -107,9 +107,8 @@
             params2 params1;
 
       (*see Theory.at_begin hook for transitive closure of classrels and arity completion*)
-      val proven_classrels' = Symreltab.join (K #1) (proven_classrels1, proven_classrels2);
-      val proven_arities' =
-        Symtab.join (K (Library.merge (eq_fst op =))) (proven_arities1, proven_arities2);
+      val proven_classrels' = Symreltab.merge (K true) (proven_classrels1, proven_classrels2);
+      val proven_arities' = Symtab.merge_list (eq_fst op =) (proven_arities1, proven_arities2);
 
       val inst_params' =
         (Symtab.join (K (Symtab.merge (K true))) (#1 inst_params1, #1 inst_params2),
@@ -188,11 +187,7 @@
   let
     fun complete (c, (_, (all_preds, all_succs))) (finished1, thy1) =
       let
-        val proven = is_classrel thy1;
-        val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds [];
-        val succs = Graph.Keys.fold (fn c2 => proven (c, c2) ? cons c2) all_succs [];
-
-        fun complete c1 c2 (finished2, thy2) =
+        fun compl c1 c2 (finished2, thy2) =
           if is_classrel thy2 (c1, c2) then (finished2, thy2)
           else
             (false,
@@ -201,12 +196,17 @@
                 (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2))
                 |> Drule.instantiate' [SOME (ctyp_of thy2 (TVar ((Name.aT, 0), [])))] []
                 |> Thm.close_derivation));
-      in fold_product complete preds succs (finished1, thy1) end;
 
-    val (finished', thy') =
-      Graph.fold complete (Sorts.classes_of (Sign.classes_of thy)) (true, thy);
+        val proven = is_classrel thy1;
+        val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds [];
+        val succs = Graph.Keys.fold (fn c2 => proven (c, c2) ? cons c2) all_succs [];
+      in
+        fold_product compl preds succs (finished1, thy1)
+      end;
   in
-    if finished' then NONE else SOME thy'
+    (case Graph.fold complete (Sorts.classes_of (Sign.classes_of thy)) (true, thy) of
+      (true, _) => NONE
+    | (_, thy') => SOME thy')
   end;
 
 
@@ -257,7 +257,8 @@
   let
     val arities = proven_arities_of thy;
     val (finished, arities') =
-      Symtab.fold (fn (t, ars) => fold (insert_arity_completions thy t) ars) arities (true, arities);
+      Symtab.fold (fn (t, ars) => fold (insert_arity_completions thy t) ars)
+        arities (true, arities);
   in
     if finished then NONE
     else SOME (map_proven_arities (K arities') thy)
@@ -388,8 +389,9 @@
     fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
     val rel = Logic.dest_classrel prop handle TERM _ => err ();
     val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
-    val (th', thy') = Global_Theory.store_thm
-      (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy;
+    val (th', thy') =
+      Global_Theory.store_thm
+        (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy;
     val th'' = th'
       |> Thm.unconstrainT
       |> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
@@ -408,8 +410,9 @@
     fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
     val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
 
-    val (th', thy') = Global_Theory.store_thm
-      (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
+    val (th', thy') =
+      Global_Theory.store_thm
+        (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
 
     val args = Name.invent_names Name.context Name.aT Ss;
     val T = Type (t, map TFree args);
diff -r 26ad3da13f47 -r 5a9964f7a691 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Tue Jan 08 13:16:39 2013 +0100
+++ b/src/Pure/consts.ML	Tue Jan 08 19:02:12 2013 +0100
@@ -318,7 +318,7 @@
     Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) =
   let
     val decls' = Name_Space.merge_tables (decls1, decls2);
-    val constraints' = Symtab.join (K fst) (constraints1, constraints2);
+    val constraints' = Symtab.merge (K true) (constraints1, constraints2);
     val rev_abbrevs' = Symtab.join (K Item_Net.merge) (rev_abbrevs1, rev_abbrevs2);
   in make_consts (decls', constraints', rev_abbrevs') end;
 
diff -r 26ad3da13f47 -r 5a9964f7a691 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Tue Jan 08 13:16:39 2013 +0100
+++ b/src/Tools/Code/code_target.ML	Tue Jan 08 19:02:12 2013 +0100
@@ -110,7 +110,7 @@
 fun merge_symbol_syntax_data
   (Symbol_Syntax_Data { class = class1, instance = instance1, tyco = tyco1, const = const1 },
     Symbol_Syntax_Data { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
-  make_symbol_syntax_data (
+  make_symbol_syntax_data ( (* FIXME proper merge order!? prefer fst!? *)
     (Symtab.join (K snd) (class1, class2),
        Symreltab.join (K snd) (instance1, instance2)),
     (Symtab.join (K snd) (tyco1, tyco2),
@@ -158,7 +158,9 @@
       module_alias = module_alias2, symbol_syntax = symbol_syntax2 }) =
   if serial1 = serial2 orelse not strict then
     make_target ((serial1, description),
-      ((merge (op =) (reserved1, reserved2), Symtab.join (K snd) (includes1, includes2)),
+      ((merge (op =) (reserved1, reserved2),
+         (* FIXME proper merge order!? prefer fst!? *)
+         Symtab.join (K snd) (includes1, includes2)),
         (Symtab.join (K snd) (module_alias1, module_alias2),
           merge_symbol_syntax_data (symbol_syntax1, symbol_syntax2))
     ))
diff -r 26ad3da13f47 -r 5a9964f7a691 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Tue Jan 08 13:16:39 2013 +0100
+++ b/src/Tools/adhoc_overloading.ML	Tue Jan 08 19:02:12 2013 +0100
@@ -53,7 +53,7 @@
   fun merge
     ({internalize = int1, externalize = ext1},
       {internalize = int2, externalize = ext2}) : T =
-    {internalize = Symtab.join (K (Library.merge (op =))) (int1, int2),
+    {internalize = Symtab.merge_list (op =) (int1, int2),
       externalize = Symtab.join merge_ext (ext1, ext2)};
 );
 
diff -r 26ad3da13f47 -r 5a9964f7a691 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Jan 08 13:16:39 2013 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Jan 08 19:02:12 2013 +0100
@@ -189,24 +189,24 @@
                      changed.commands.exists(snapshot.node.commands.contains)))
                   Swing_Thread.later { overview.delay_repaint.invoke() }
 
-                JEdit_Lib.visible_range(text_area) match {
-                  case Some(visible) =>
-                    if (changed.assignment) JEdit_Lib.invalidate_range(text_area, visible)
-                    else {
-                      val visible_cmds =
-                        snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
-                      if (visible_cmds.exists(changed.commands)) {
-                        for {
-                          line <- 0 until text_area.getVisibleLines
-                          start = text_area.getScreenLineStartOffset(line) if start >= 0
-                          end = text_area.getScreenLineEndOffset(line) if end >= 0
-                          range = Text.Range(start, end)
-                          line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
-                          if line_cmds.exists(changed.commands)
-                        } text_area.invalidateScreenLineRange(line, line)
-                      }
+                val visible_lines = text_area.getVisibleLines
+                if (visible_lines > 0) {
+                  if (changed.assignment) text_area.invalidateScreenLineRange(0, visible_lines)
+                  else {
+                    val visible_range = JEdit_Lib.visible_range(text_area).get
+                    val visible_cmds =
+                      snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
+                    if (visible_cmds.exists(changed.commands)) {
+                      for {
+                        line <- 0 until visible_lines
+                        start = text_area.getScreenLineStartOffset(line) if start >= 0
+                        end = text_area.getScreenLineEndOffset(line) if end >= 0
+                        range = Text.Range(start, end)
+                        line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
+                        if line_cmds.exists(changed.commands)
+                      } text_area.invalidateScreenLineRange(line, line)
                     }
-                  case None =>
+                  }
                 }
               }
             }
diff -r 26ad3da13f47 -r 5a9964f7a691 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Tue Jan 08 13:16:39 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Tue Jan 08 19:02:12 2013 +0100
@@ -55,7 +55,7 @@
 
   def change_font_size(view: View, change: Int => Int)
   {
-    val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5
+    val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5 min 250
     jEdit.setIntegerProperty("view.fontsize", size)
     jEdit.propertiesChanged()
     jEdit.saveSettings()
diff -r 26ad3da13f47 -r 5a9964f7a691 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Tue Jan 08 13:16:39 2013 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue Jan 08 19:02:12 2013 +0100
@@ -93,7 +93,8 @@
         case _: Session.Global_Options =>
           Swing_Thread.later { handle_resize() }
         case changed: Session.Commands_Changed =>
-          Swing_Thread.later { handle_update(do_update, Some(changed.commands)) }
+          val restriction = if (changed.assignment) None else Some(changed.commands)
+          Swing_Thread.later { handle_update(do_update, restriction) }
         case Session.Caret_Focus =>
           Swing_Thread.later { handle_update(do_update, None) }
         case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)