# HG changeset patch
# User wenzelm
# Date 1369076051 -7200
# Node ID 895d12fc0dd7cd508ae7d1e2d130562472a49ccc
# Parent  d9c04fb297e1e4247eb8a80809aeafaf11758ba8# Parent  9ec2d47de6a72c5071197065aac02ea8ba634a22
merged

diff -r d9c04fb297e1 -r 895d12fc0dd7 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Mon May 20 16:12:33 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Mon May 20 20:54:11 2013 +0200
@@ -2695,8 +2695,8 @@
 
         val in_bd_tacs = map7 (fn i => fn isNode_hsets => fn carT_def =>
             fn card_of_carT => fn mor_image => fn Rep_inverse => fn mor_hsets =>
-          K (mk_in_bd_tac lthy (* FIXME proper context!? *)
-            (nth isNode_hsets (i - 1)) isNode_hsets carT_def
+          (fn {context = ctxt, prems = _} =>
+            mk_in_bd_tac ctxt (nth isNode_hsets (i - 1)) isNode_hsets carT_def
             card_of_carT mor_image Rep_inverse mor_hsets
             sbd_Cnotzero sbd_Card_order mor_Rep_thm coalgT_thm mor_T_final_thm tcoalg_thm))
           ks isNode_hset_thmss carT_defs card_of_carT_thms
diff -r d9c04fb297e1 -r 895d12fc0dd7 src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Mon May 20 16:12:33 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Mon May 20 20:54:11 2013 +0200
@@ -167,9 +167,9 @@
 
   val standard_binding: binding
   val equal_binding: binding
-  val parse_binding: Token.T list -> binding * Token.T list
-  val parse_binding_colon: Token.T list -> binding * Token.T list
-  val parse_opt_binding_colon: Token.T list -> binding * Token.T list
+  val parse_binding: binding parser
+  val parse_binding_colon: binding parser
+  val parse_opt_binding_colon: binding parser
 
   val typedef: binding * (string * sort) list * mixfix -> term ->
     (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
diff -r d9c04fb297e1 -r 895d12fc0dd7 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Mon May 20 16:12:33 2013 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Mon May 20 20:54:11 2013 +0200
@@ -3487,7 +3487,7 @@
                                      (@{cpat "?prec::nat"}, p),
                                      (@{cpat "?ss::nat list"}, s)])
               @{thm "approx_form"}) i
-          THEN simp_tac @{context} i) st
+          THEN simp_tac (put_simpset (simpset_of @{context}) ctxt) i) st
        end
 
      | SOME t => if length vs <> 1 then raise (TERM ("More than one variable used for taylor series expansion", [prop_of st]))
@@ -3531,7 +3531,7 @@
       REPEAT (FIRST' [etac @{thm intervalE},
                       etac @{thm meta_eqE},
                       rtac @{thm impI}] i)
-      THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
+      THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) ctxt i
       THEN DETERM (TRY (filter_prems_tac (K false) i))
       THEN DETERM (Reflection.gen_reify_tac ctxt form_equations NONE i)
       THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
@@ -3621,33 +3621,33 @@
        |> HOLogic.dest_Trueprop
        |> HOLogic.dest_eq |> snd
 
-  fun apply_tactic context term tactic = cterm_of context term
+  fun apply_tactic ctxt term tactic =
+    cterm_of (Proof_Context.theory_of ctxt) term
     |> Goal.init
     |> SINGLE tactic
     |> the |> prems_of |> hd
 
-  fun prepare_form context term = apply_tactic context term (
+  fun prepare_form ctxt term = apply_tactic ctxt term (
       REPEAT (FIRST' [etac @{thm intervalE}, etac @{thm meta_eqE}, rtac @{thm impI}] 1)
-      THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems 1) @{context} 1
+      THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems 1) ctxt 1
       THEN DETERM (TRY (filter_prems_tac (K false) 1)))
 
-  fun reify_form context term = apply_tactic context term
-     (Reflection.gen_reify_tac @{context} form_equations NONE 1)
+  fun reify_form ctxt term = apply_tactic ctxt term
+     (Reflection.gen_reify_tac ctxt form_equations NONE 1)
 
   fun approx_form prec ctxt t =
           realify t
-       |> prepare_form (Proof_Context.theory_of ctxt)
-       |> (fn arith_term =>
-          reify_form (Proof_Context.theory_of ctxt) arith_term
-       |> HOLogic.dest_Trueprop |> dest_interpret_form
-       |> (fn (data, xs) =>
-          mk_approx_form_eval prec data (HOLogic.mk_list @{typ "(float * float) option"}
-            (map (fn _ => @{term "None :: (float * float) option"}) (HOLogic.dest_list xs)))
-       |> approximate ctxt
-       |> HOLogic.dest_list
-       |> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term)
-       |> map (fn (elem, s) => @{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ elem $ mk_result prec (dest_ivl s))
-       |> foldr1 HOLogic.mk_conj))
+       |> prepare_form ctxt
+       |> (fn arith_term => reify_form ctxt arith_term
+           |> HOLogic.dest_Trueprop |> dest_interpret_form
+           |> (fn (data, xs) =>
+              mk_approx_form_eval prec data (HOLogic.mk_list @{typ "(float * float) option"}
+                (map (fn _ => @{term "None :: (float * float) option"}) (HOLogic.dest_list xs)))
+           |> approximate ctxt
+           |> HOLogic.dest_list
+           |> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term)
+           |> map (fn (elem, s) => @{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ elem $ mk_result prec (dest_ivl s))
+           |> foldr1 HOLogic.mk_conj))
 
   fun approx_arith prec ctxt t = realify t
        |> Reflection.gen_reify ctxt form_equations
diff -r d9c04fb297e1 -r 895d12fc0dd7 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Mon May 20 16:12:33 2013 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Mon May 20 20:54:11 2013 +0200
@@ -872,6 +872,7 @@
   val less_iff_diff_less_0 = mk_meta_eq @{thm "less_iff_diff_less_0"}
   val le_iff_diff_le_0 = mk_meta_eq @{thm "le_iff_diff_le_0"}
   val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"}
+  val ss = simpset_of @{context}
 in
 fun field_isolate_conv phi ctxt vs ct = case term_of ct of
   Const(@{const_name Orderings.less},_)$a$b =>
@@ -880,7 +881,7 @@
        val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
        val nth = Conv.fconv_rule
          (Conv.arg_conv (Conv.arg1_conv
-              (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
+              (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
        val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    in rth end
 | Const(@{const_name Orderings.less_eq},_)$a$b =>
@@ -889,7 +890,7 @@
        val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
        val nth = Conv.fconv_rule
          (Conv.arg_conv (Conv.arg1_conv
-              (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
+              (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
        val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    in rth end
 
@@ -899,7 +900,7 @@
        val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
        val nth = Conv.fconv_rule
          (Conv.arg_conv (Conv.arg1_conv
-              (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
+              (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
        val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    in rth end
 | @{term "Not"} $(Const(@{const_name HOL.eq},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
diff -r d9c04fb297e1 -r 895d12fc0dd7 src/HOL/Prolog/prolog.ML
--- a/src/HOL/Prolog/prolog.ML	Mon May 20 16:12:33 2013 +0200
+++ b/src/HOL/Prolog/prolog.ML	Mon May 20 20:54:11 2013 +0200
@@ -65,7 +65,8 @@
         @{thm all_conj_distrib}, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
         @{thm imp_conjL} RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
         @{thm imp_conjR},        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
-        @{thm imp_all}];         (* "((!x. D) :- G) = (!x. D :- G)" *)
+        @{thm imp_all}]          (* "((!x. D) :- G) = (!x. D :- G)" *)
+  |> simpset_of;
 
 
 (*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} =>
@@ -114,7 +115,7 @@
                 rtac allI,                      (* "(!!x. P x) ==> ! x. P x" *)
                 rtac exI,                       (* "P x ==> ? x. P x" *)
                 rtac impI THEN'                 (* "(P ==> Q) ==> P --> Q" *)
-                  asm_full_simp_tac atomize_ss THEN'    (* atomize the asms *)
+                  asm_full_simp_tac (put_simpset atomize_ss ctxt) THEN'    (* atomize the asms *)
                   (REPEAT_DETERM o (etac conjE))        (* split the asms *)
                 ])
         ORELSE' resolve_tac [disjI1,disjI2]     (* "P ==> P | Q","Q ==> P | Q"*)
diff -r d9c04fb297e1 -r 895d12fc0dd7 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Mon May 20 16:12:33 2013 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Mon May 20 20:54:11 2013 +0200
@@ -255,11 +255,11 @@
     val unfold =
       (cterm_instantiate' (map (SOME o cert) [uncurry, F, curry]) fixp_eq
         OF [mono_thm, f_def])
-      |> Tactic.rule_by_tactic lthy (Simplifier.simp_tac (put_simpset curry_uncurry_ss lthy) 1);
+      |> Tactic.rule_by_tactic lthy' (Simplifier.simp_tac (put_simpset curry_uncurry_ss lthy') 1);
 
     val mk_raw_induct =
       mk_curried_induct args args_ctxt (cert curry) (cert uncurry)
-      #> singleton (Variable.export args_ctxt lthy)
+      #> singleton (Variable.export args_ctxt lthy')
       #> (fn thm => cterm_instantiate' [SOME (cert F)] thm OF [mono_thm, f_def])
       #> Drule.rename_bvars' (map SOME (fname :: argnames @ argnames))
 
diff -r d9c04fb297e1 -r 895d12fc0dd7 src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Mon May 20 16:12:33 2013 +0200
+++ b/src/HOL/Tools/groebner.ML	Mon May 20 20:54:11 2013 +0200
@@ -1002,6 +1002,8 @@
  | _=> raise CTERM ("ideal_tac - lhs",[t])
  fun exitac NONE = no_tac
    | exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1
+
+ val claset = claset_of @{context}
 in
 fun ideal_tac add_ths del_ths ctxt =
   presimplify ctxt add_ths del_ths
@@ -1023,10 +1025,10 @@
         THEN ring_tac add_ths del_ths ctxt 1
    end
   in
-     clarify_tac @{context} i
+     clarify_tac (put_claset claset ctxt) i
      THEN Object_Logic.full_atomize_tac i
      THEN asm_full_simp_tac (put_simpset (#poly_eq_ss thy) ctxt) i
-     THEN clarify_tac @{context} i
+     THEN clarify_tac (put_claset claset ctxt) i
      THEN (REPEAT (CONVERSION (#unwind_conv thy ctxt) i))
      THEN SUBPROOF poly_exists_tac ctxt i
   end
diff -r d9c04fb297e1 -r 895d12fc0dd7 src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Mon May 20 16:12:33 2013 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Mon May 20 20:54:11 2013 +0200
@@ -722,8 +722,8 @@
                       @{thm rename_guarantees_eq_rename_inv},
                       @{thm bij_imp_bij_inv}, @{thm surj_rename},
                       @{thm inv_inv_eq}]) 1,
-    asm_simp_tac  (* FIXME ctxt !!? *)
-        (@{context} addsimps [@{thm o_def}, @{thm non_dummy_def}, @{thm guarantees_Int_right}]) 1]
+    asm_simp_tac
+        (ctxt addsimps [@{thm o_def}, @{thm non_dummy_def}, @{thm guarantees_Int_right}]) 1]
 *}
 
 method_setup rename_client_map = {*
diff -r d9c04fb297e1 -r 895d12fc0dd7 src/Pure/Concurrent/time_limit.ML
--- a/src/Pure/Concurrent/time_limit.ML	Mon May 20 16:12:33 2013 +0200
+++ b/src/Pure/Concurrent/time_limit.ML	Mon May 20 20:54:11 2013 +0200
@@ -32,8 +32,7 @@
     in
       if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
       then raise TimeOut
-      else if Exn.is_interrupt_exn test then Exn.interrupt ()
-      else Exn.release result
+      else (Exn.release test; Exn.release result)
     end);
 
 end;
diff -r d9c04fb297e1 -r 895d12fc0dd7 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Mon May 20 16:12:33 2013 +0200
+++ b/src/Pure/System/session.ML	Mon May 20 20:54:11 2013 +0200
@@ -54,7 +54,6 @@
   Present.finish ();
   Keyword.status ();
   Outer_Syntax.check_syntax ();
-  Options.reset_default ();
   Future.shutdown ();
   Event_Timer.shutdown ();
   session_finished := true);
diff -r d9c04fb297e1 -r 895d12fc0dd7 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Mon May 20 16:12:33 2013 +0200
+++ b/src/Pure/System/session.scala	Mon May 20 20:54:11 2013 +0200
@@ -177,6 +177,7 @@
     version: Document.Version)
   private case class Messages(msgs: List[Isabelle_Process.Message])
   private case class Finished_Scala(id: String, tag: Invoke_Scala.Tag.Value, result: String)
+  private case class Update_Options(options: Options)
 
   private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
   {
@@ -415,8 +416,10 @@
           receiver.cancel()
           reply(())
 
-        case Session.Global_Options(options) if prover.isDefined =>
+        case Update_Options(options) if prover.isDefined =>
           if (is_ready) prover.get.options(options)
+          global_options.event(Session.Global_Options(options))
+          reply(())
 
         case Cancel_Execution if prover.isDefined =>
           prover.get.cancel_execution()
@@ -470,13 +473,11 @@
 
   def start(args: List[String])
   {
-    global_options += session_actor
     session_actor ! Start(args)
   }
 
   def stop()
   {
-    global_options -= session_actor
     commands_changed_buffer !? Stop
     change_parser !? Stop
     session_actor !? Stop
@@ -487,6 +488,9 @@
   def update(edits: List[Document.Edit_Text])
   { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(edits) }
 
+  def update_options(options: Options)
+  { session_actor !? Update_Options(options) }
+
   def dialog_result(id: Document.ID, serial: Long, result: String)
   { session_actor ! Session.Dialog_Result(id, serial, result) }
 }
diff -r d9c04fb297e1 -r 895d12fc0dd7 src/Pure/build
--- a/src/Pure/build	Mon May 20 16:12:33 2013 +0200
+++ b/src/Pure/build	Mon May 20 20:54:11 2013 +0200
@@ -80,6 +80,7 @@
       -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => Posix.Process.exit 0w1;" \
       -e "ml_prompts \"ML> \" \"ML# \";" \
       -e "Command_Line.tool0 Session.finish;" \
+      -e "Options.reset_default ();" \
       -q -w RAW_ML_SYSTEM "$OUTPUT"
   fi
 fi
diff -r d9c04fb297e1 -r 895d12fc0dd7 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Mon May 20 16:12:33 2013 +0200
+++ b/src/Pure/raw_simplifier.ML	Mon May 20 20:54:11 2013 +0200
@@ -510,10 +510,6 @@
 fun add_prems ths =
   map_simpset1 (fn (rules, prems, bounds, depth) => (rules, ths @ prems, bounds, depth));
 
-fun activate_context thy ctxt = ctxt  (* FIXME ?? *)
-  |> Context.raw_transfer (Theory.merge (thy, Proof_Context.theory_of ctxt))
-  |> Context_Position.set_visible false;
-
 
 (* maintain simp rules *)
 
@@ -545,7 +541,6 @@
 
 fun decomp_simp thm =
   let
-    val thy = Thm.theory_of_thm thm;
     val prop = Thm.prop_of thm;
     val prems = Logic.strip_imp_prems prop;
     val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
@@ -557,12 +552,12 @@
       var_perm (term_of elhs, erhs) andalso
       not (term_of elhs aconv erhs) andalso
       not (is_Var (term_of elhs));
-  in (thy, prems, term_of lhs, elhs, term_of rhs, perm) end;
+  in (prems, term_of lhs, elhs, term_of rhs, perm) end;
 
 end;
 
 fun decomp_simp' thm =
-  let val (_, _, lhs, _, rhs, _) = decomp_simp thm in
+  let val (_, lhs, _, rhs, _) = decomp_simp thm in
     if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
     else (lhs, rhs)
   end;
@@ -572,13 +567,13 @@
     (case mk_eq_True ctxt thm of
       NONE => []
     | SOME eq_True =>
-        let val (_, _, lhs, elhs, _, _) = decomp_simp eq_True;
+        let val (_, lhs, elhs, _, _) = decomp_simp eq_True;
         in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end)
   end;
 
 (*create the rewrite rule and possibly also the eq_True variant,
   in case there are extra vars on the rhs*)
-fun rrule_eq_True (thm, name, lhs, elhs, rhs, ctxt, thm2) =
+fun rrule_eq_True ctxt thm name lhs elhs rhs thm2 =
   let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in
     if rewrite_rule_extra_vars [] lhs rhs then
       mk_eq_True ctxt (thm2, name) @ [rrule]
@@ -586,18 +581,18 @@
   end;
 
 fun mk_rrule ctxt (thm, name) =
-  let val (_, prems, lhs, elhs, rhs, perm) = decomp_simp thm in
+  let val (prems, lhs, elhs, rhs, perm) = decomp_simp thm in
     if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
     else
       (*weak test for loops*)
       if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (term_of elhs)
       then mk_eq_True ctxt (thm, name)
-      else rrule_eq_True (thm, name, lhs, elhs, rhs, ctxt, thm)
+      else rrule_eq_True ctxt thm name lhs elhs rhs thm
   end;
 
 fun orient_rrule ctxt (thm, name) =
   let
-    val (thy, prems, lhs, elhs, rhs, perm) = decomp_simp thm;
+    val (prems, lhs, elhs, rhs, perm) = decomp_simp thm;
     val Simpset (_, {mk_rews = {reorient, mk_sym, ...}, ...}) = simpset_of ctxt;
   in
     if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
@@ -608,9 +603,9 @@
         (case mk_sym ctxt thm of
           NONE => []
         | SOME thm' =>
-            let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm'
-            in rrule_eq_True (thm', name, lhs', elhs', rhs', ctxt, thm) end)
-    else rrule_eq_True (thm, name, lhs, elhs, rhs, ctxt, thm)
+            let val (_, lhs', elhs', rhs', _) = decomp_simp thm'
+            in rrule_eq_True ctxt thm' name lhs' elhs' rhs' thm end)
+    else rrule_eq_True ctxt thm name lhs elhs rhs thm
   end;
 
 fun extract_rews (ctxt, thms) =
@@ -886,7 +881,7 @@
 (* mk_procrule *)
 
 fun mk_procrule ctxt thm =
-  let val (_, prems, lhs, elhs, rhs, _) = decomp_simp thm in
+  let val (prems, lhs, elhs, rhs, _) = decomp_simp thm in
     if rewrite_rule_extra_vars prems lhs rhs
     then (cond_warn_thm ctxt (fn () => "Extra vars on rhs:") thm; [])
     else [mk_rrule2 {thm = thm, name = "", lhs = lhs, elhs = elhs, perm = false}]
@@ -934,7 +929,7 @@
   IMPORTANT: rewrite rules must not introduce new Vars or TVars!
 *)
 
-fun rewritec (prover, thyt, maxt) ctxt t =
+fun rewritec (prover, maxt) ctxt t =
   let
     val Simpset ({rules, ...}, {congs, procs, termless, ...}) = simpset_of ctxt;
     val eta_thm = Thm.eta_conversion t;
@@ -1007,7 +1002,7 @@
 
     fun proc_rews [] = NONE
       | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
-          if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then
+          if Pattern.matches (Proof_Context.theory_of ctxt) (Thm.term_of lhs, Thm.term_of t) then
             (debug_term ctxt false (fn () => "Trying procedure " ^ quote name ^ " on:") eta_t;
              case proc ctxt eta_t' of
                NONE => (debug ctxt false (fn () => "FAILED"); proc_rews ps)
@@ -1063,20 +1058,20 @@
 fun transitive2 thm = transitive1 (SOME thm);
 fun transitive3 thm = transitive1 thm o SOME;
 
-fun bottomc ((simprem, useprem, mutsimp), prover, thy, maxidx) =
+fun bottomc ((simprem, useprem, mutsimp), prover, maxidx) =
   let
     fun botc skel ctxt t =
           if is_Var skel then NONE
           else
           (case subc skel ctxt t of
              some as SOME thm1 =>
-               (case rewritec (prover, thy, maxidx) ctxt (Thm.rhs_of thm1) of
+               (case rewritec (prover, maxidx) ctxt (Thm.rhs_of thm1) of
                   SOME (thm2, skel2) =>
                     transitive2 (Thm.transitive thm1 thm2)
                       (botc skel2 ctxt (Thm.rhs_of thm2))
                 | NONE => some)
            | NONE =>
-               (case rewritec (prover, thy, maxidx) ctxt t of
+               (case rewritec (prover, maxidx) ctxt t of
                   SOME (thm2, skel2) => transitive2 thm2
                     (botc skel2 ctxt (Thm.rhs_of thm2))
                 | NONE => NONE))
@@ -1197,7 +1192,7 @@
               Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq));
             val dprem = Option.map (disch false prem)
           in
-            (case rewritec (prover, thy, maxidx) ctxt' concl' of
+            (case rewritec (prover, maxidx) ctxt' concl' of
               NONE => rebuild prems concl' rrss asms ctxt (dprem eq)
             | SOME (eq', _) => transitive2 (fold (disch false)
                   prems (the (transitive3 (dprem eq) eq')))
@@ -1305,10 +1300,18 @@
 
 fun rewrite_cterm mode prover raw_ctxt raw_ct =
   let
-    val thy = Thm.theory_of_cterm raw_ct;
+    val ctxt =
+      raw_ctxt
+      |> Context_Position.set_visible false
+      |> inc_simp_depth;
+    val thy = Proof_Context.theory_of ctxt;
+
     val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
     val {maxidx, ...} = Thm.rep_cterm ct;
-    val ctxt = inc_simp_depth (activate_context thy raw_ctxt);
+    val _ =
+      Theory.subthy (theory_of_cterm ct, thy) orelse
+        raise CTERM ("rewrite_cterm: bad background theory", [ct]);
+
     val depth = simp_depth ctxt;
     val _ =
       if depth mod 20 = 0 then
@@ -1316,7 +1319,7 @@
       else ();
     val _ = trace_cterm ctxt false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ct;
     val _ = check_bounds ctxt ct;
-  in bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ctxt ct end;
+  in bottomc (mode, Option.map Drule.flexflex_unique oo prover, maxidx) ctxt ct end;
 
 val simple_prover =
   SINGLE o (fn ctxt => ALLGOALS (resolve_tac (prems_of ctxt)));
diff -r d9c04fb297e1 -r 895d12fc0dd7 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Mon May 20 16:12:33 2013 +0200
+++ b/src/Pure/tactic.ML	Mon May 20 20:54:11 2013 +0200
@@ -85,8 +85,9 @@
 (*Makes a rule by applying a tactic to an existing rule*)
 fun rule_by_tactic ctxt tac rl =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val ctxt' = Variable.declare_thm rl ctxt;
-    val ((_, [st]), ctxt'') = Variable.import true [rl] ctxt';
+    val ((_, [st]), ctxt'') = Variable.import true [Thm.transfer thy rl] ctxt';
   in
     (case Seq.pull (tac st) of
       NONE => raise THM ("rule_by_tactic", 0, [rl])
diff -r d9c04fb297e1 -r 895d12fc0dd7 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Mon May 20 16:12:33 2013 +0200
+++ b/src/Tools/Code/code_printer.ML	Mon May 20 20:54:11 2013 +0200
@@ -101,8 +101,8 @@
     | Complex_const_syntax of activated_complex_const_syntax
   type tyco_syntax
   val requires_args: const_syntax -> int
-  val parse_const_syntax: Token.T list -> const_syntax * Token.T list
-  val parse_tyco_syntax: Token.T list -> tyco_syntax * Token.T list
+  val parse_const_syntax: const_syntax parser
+  val parse_tyco_syntax: tyco_syntax parser
   val plain_const_syntax: string -> const_syntax
   val simple_const_syntax: simple_const_syntax -> const_syntax
   val complex_const_syntax: complex_const_syntax -> const_syntax
diff -r d9c04fb297e1 -r 895d12fc0dd7 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Mon May 20 16:12:33 2013 +0200
+++ b/src/Tools/jEdit/src/active.scala	Mon May 20 20:54:11 2013 +0200
@@ -77,14 +77,10 @@
                     else text_area.setSelectedText(text)
                 }
 
+              case Protocol.Dialog(id, serial, result) =>
+                model.session.dialog_result(id, serial, result)
+
               case _ =>
-                // FIXME pattern match problem in scala-2.9.2 (!??)
-                elem match {
-                  case Protocol.Dialog(id, serial, result) =>
-                    model.session.dialog_result(id, serial, result)
-
-                  case _ =>
-                }
             }
           }
         }
diff -r d9c04fb297e1 -r 895d12fc0dd7 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon May 20 16:12:33 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon May 20 20:54:11 2013 +0200
@@ -196,7 +196,7 @@
               }
 
             case Session.Ready =>
-              PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
+              PIDE.session.update_options(PIDE.options.value)
               PIDE.init_models(JEdit_Lib.jedit_buffers().toList)
               Swing_Thread.later { delay_load.invoke() }
 
@@ -270,7 +270,7 @@
           }
 
         case msg: PropertiesChanged =>
-          PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
+          PIDE.session.update_options(PIDE.options.value)
 
         case _ =>
       }
diff -r d9c04fb297e1 -r 895d12fc0dd7 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon May 20 16:12:33 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Mon May 20 20:54:11 2013 +0200
@@ -481,17 +481,12 @@
                 (None, Some(bad_color))
               case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
                 (None, Some(intensify_color))
-              case (acc, Text.Info(_, elem @ XML.Elem(Markup(Markup.DIALOG, _), _))) =>
-                // FIXME pattern match problem in scala-2.9.2 (!??)
-                elem match {
-                  case Protocol.Dialog(_, serial, result) =>
-                    command_state.results.get(serial) match {
-                      case Some(Protocol.Dialog_Result(res)) if res == result =>
-                        (None, Some(active_result_color))
-                      case _ =>
-                        (None, Some(active_color))
-                    }
-                  case _ => acc
+              case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
+                command_state.results.get(serial) match {
+                  case Some(Protocol.Dialog_Result(res)) if res == result =>
+                    (None, Some(active_result_color))
+                  case _ =>
+                    (None, Some(active_color))
                 }
               case (_, Text.Info(_, XML.Elem(markup, _))) if active_include(markup.name) =>
                 (None, Some(active_color))
diff -r d9c04fb297e1 -r 895d12fc0dd7 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Mon May 20 16:12:33 2013 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Mon May 20 20:54:11 2013 +0200
@@ -252,15 +252,15 @@
   val dummy = writeln "  Proving the elimination rule...";
 
   (*Breaks down logical connectives in the monotonic function*)
-  val basic_elim_tac =
+  fun basic_elim_tac ctxt =
       REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)
-                ORELSE' bound_hyp_subst_tac ctxt1))
+                ORELSE' bound_hyp_subst_tac ctxt))
       THEN prune_params_tac
           (*Mutual recursion: collapse references to Part(D,h)*)
       THEN (PRIMITIVE (fold_rule part_rec_defs));
 
   (*Elimination*)
-  val elim = rule_by_tactic (Proof_Context.init_global thy1) basic_elim_tac
+  val elim = rule_by_tactic (Proof_Context.init_global thy1) (basic_elim_tac ctxt1)
                  (unfold RS Ind_Syntax.equals_CollectD)
 
   (*Applies freeness of the given constructors, which *must* be unfolded by
@@ -269,7 +269,7 @@
     Proposition A should have the form t:Si where Si is an inductive set*)
   fun make_cases ctxt A =
     rule_by_tactic ctxt
-      (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac ctxt) THEN basic_elim_tac)
+      (basic_elim_tac ctxt THEN ALLGOALS (asm_full_simp_tac ctxt) THEN basic_elim_tac ctxt)
       (Thm.assume A RS elim)
       |> Drule.export_without_context_open;