# HG changeset patch
# User wenzelm
# Date 1397133611 -7200
# Node ID b62c4e6d1b556fda14aaac305aa2df0e240338a3
# Parent  535cfc7fc30130f08b2e75fe70c9e4d3b3055a89# Parent  db929027e70131457e65cbbefdf2b77d5d2c211e
merged

diff -r 535cfc7fc301 -r b62c4e6d1b55 NEWS
--- a/NEWS	Thu Apr 10 11:34:55 2014 +0200
+++ b/NEWS	Thu Apr 10 14:40:11 2014 +0200
@@ -25,6 +25,10 @@
 supports input methods via ` (backquote), or << and >> (double angle
 brackets).
 
+* The outer syntax categories "text" (for formal comments and document
+markup commands) and "altstring" (for literal fact references) allow
+cartouches as well, in addition to the traditional mix of quotations.
+
 * More static checking of proof methods, which allows the system to
 form a closure over the concrete syntax.  Method arguments should be
 processed in the original proof context as far as possible, before
@@ -110,6 +114,9 @@
 
 * Support for Navigator plugin (with toolbar buttons).
 
+* More support for remote files (e.g. http) using standard Java
+networking operations instead of jEdit virtual file-systems.
+
 
 *** Pure ***
 
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Doc/Implementation/Tactic.thy
--- a/src/Doc/Implementation/Tactic.thy	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Doc/Implementation/Tactic.thy	Thu Apr 10 14:40:11 2014 +0200
@@ -175,7 +175,7 @@
   @{index_ML_type tactic: "thm -> thm Seq.seq"} \\
   @{index_ML no_tac: tactic} \\
   @{index_ML all_tac: tactic} \\
-  @{index_ML print_tac: "string -> tactic"} \\[1ex]
+  @{index_ML print_tac: "Proof.context -> string -> tactic"} \\[1ex]
   @{index_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex]
   @{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\
   @{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\
@@ -200,7 +200,7 @@
   \item @{ML all_tac} is a tactic that always succeeds, returning a
   singleton sequence with unchanged goal state.
 
-  \item @{ML print_tac}~@{text "message"} is like @{ML all_tac}, but
+  \item @{ML print_tac}~@{text "ctxt message"} is like @{ML all_tac}, but
   prints a message together with the goal state on the tracing
   channel.
 
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Thu Apr 10 14:40:11 2014 +0200
@@ -265,14 +265,14 @@
 
 text {* Large chunks of plain @{syntax text} are usually given
   @{syntax verbatim}, i.e.\ enclosed in @{verbatim "{"}@{verbatim
-  "*"}~@{text "\<dots>"}~@{verbatim "*"}@{verbatim "}"}.  For convenience,
-  any of the smaller text units conforming to @{syntax nameref} are
-  admitted as well.  A marginal @{syntax comment} is of the form
-  @{verbatim "--"}~@{syntax text}.  Any number of these may occur
-  within Isabelle/Isar commands.
+  "*"}~@{text "\<dots>"}~@{verbatim "*"}@{verbatim "}"}, or as @{syntax
+  cartouche} @{text "\<open>\<dots>\<close>"}.  For convenience, any of the smaller text
+  units conforming to @{syntax nameref} are admitted as well.  A
+  marginal @{syntax comment} is of the form @{verbatim "--"}~@{syntax
+  text}.  Any number of these may occur within Isabelle/Isar commands.
 
   @{rail \<open>
-    @{syntax_def text}: @{syntax verbatim} | @{syntax nameref}
+    @{syntax_def text}: @{syntax verbatim} | @{syntax cartouche} | @{syntax nameref}
     ;
     @{syntax_def comment}: '--' @{syntax text}
   \<close>}
@@ -424,9 +424,9 @@
 
   \item selections from named facts @{text "a(i)"} or @{text "a(j - k)"},
 
-  \item literal fact propositions using @{syntax_ref altstring} syntax
-  @{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} (see also method
-  @{method_ref fact}).
+  \item literal fact propositions using token syntax @{syntax_ref altstring}
+  @{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} or @{syntax_ref cartouche}
+  @{text "\<open>\<phi>\<close>"} (see also method @{method_ref fact}).
 
   \end{enumerate}
 
@@ -451,7 +451,8 @@
     @{syntax_def thmdef}: thmbind '='
     ;
     @{syntax_def thmref}:
-      (@{syntax nameref} selection? | @{syntax altstring}) @{syntax attributes}? |
+      (@{syntax nameref} selection? | @{syntax altstring} | @{syntax cartouche})
+        @{syntax attributes}? |
       '[' @{syntax attributes} ']'
     ;
     @{syntax_def thmrefs}: @{syntax thmref} +
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/HOL/HOLCF/Domain_Aux.thy
--- a/src/HOL/HOLCF/Domain_Aux.thy	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/HOLCF/Domain_Aux.thy	Thu Apr 10 14:40:11 2014 +0200
@@ -350,6 +350,4 @@
 ML_file "Tools/Domain/domain_constructors.ML"
 ML_file "Tools/Domain/domain_induction.ML"
 
-setup Domain_Take_Proofs.setup
-
 end
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Thu Apr 10 14:40:11 2014 +0200
@@ -61,7 +61,6 @@
   val get_deflation_thms : theory -> thm list
   val map_ID_add : attribute
   val get_map_ID_thms : theory -> thm list
-  val setup : theory -> theory
 end
 
 structure Domain_Take_Proofs : DOMAIN_TAKE_PROOFS =
@@ -148,7 +147,7 @@
 val map_ID_add = Map_Id_Data.add
 val get_map_ID_thms = Map_Id_Data.get o Proof_Context.init_global
 
-val setup = DeflMapData.setup #> Map_Id_Data.setup
+val _ = Theory.setup (DeflMapData.setup #> Map_Id_Data.setup)
 
 (******************************************************************************)
 (************************** building types and terms **************************)
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Thu Apr 10 14:40:11 2014 +0200
@@ -81,9 +81,9 @@
 val weak_congs   = [@{thm "if_weak_cong"}]
 
 (* debugging *)
-fun DEBUG_tac (msg,tac) = 
-    CHANGED (EVERY [print_tac ("before "^msg), tac, print_tac ("after "^msg)]); 
-fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
+fun DEBUG ctxt (msg,tac) = 
+    CHANGED (EVERY [print_tac ctxt ("before "^msg), tac, print_tac ctxt ("after "^msg)]); 
+fun NO_DEBUG _ (_,tac) = CHANGED tac; 
 
 
 (* simproc that deals with instances of permutations in front *)
@@ -170,8 +170,8 @@
 
 
 (* main simplification tactics for permutations *)
-fun perm_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical (perm_simp stac ctxt i));
-fun eqvt_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical (eqvt_simp stac ctxt i)); 
+fun perm_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical ctxt (perm_simp stac ctxt i));
+fun eqvt_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical ctxt (eqvt_simp stac ctxt i)); 
 
 val perm_simp_tac_i          = perm_simp_tac_gen_i simp_tac
 val perm_asm_simp_tac_i      = perm_simp_tac_gen_i asm_simp_tac
@@ -253,12 +253,12 @@
   let fun perm_extend_simp_tac_aux tactical ctxt n = 
           if n=0 then K all_tac
           else DETERM o 
-               (FIRST'[fn i => tactical ("splitting conjunctions on the rhs", rtac conjI i),
-                       fn i => tactical (perm_simp asm_full_simp_tac ctxt i),
-                       fn i => tactical (perm_compose_tac ctxt i),
-                       fn i => tactical (apply_cong_tac i), 
-                       fn i => tactical (unfold_perm_fun_def_tac i),
-                       fn i => tactical (ext_fun_tac i)]
+               (FIRST'[fn i => tactical ctxt ("splitting conjunctions on the rhs", rtac conjI i),
+                       fn i => tactical ctxt (perm_simp asm_full_simp_tac ctxt i),
+                       fn i => tactical ctxt (perm_compose_tac ctxt i),
+                       fn i => tactical ctxt (apply_cong_tac i), 
+                       fn i => tactical ctxt (unfold_perm_fun_def_tac i),
+                       fn i => tactical ctxt (ext_fun_tac i)]
                       THEN_ALL_NEW (TRY o (perm_extend_simp_tac_aux tactical ctxt (n-1))))
   in perm_extend_simp_tac_aux tactical ctxt 10 end;
 
@@ -270,11 +270,11 @@
   let 
      val simps        = [supports_def, Thm.symmetric fresh_def, fresh_prod]
   in
-      EVERY [tactical ("unfolding of supports   ", simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps) i),
-             tactical ("stripping of foralls    ", REPEAT_DETERM (rtac allI i)),
-             tactical ("geting rid of the imps  ", rtac impI i),
-             tactical ("eliminating conjuncts   ", REPEAT_DETERM (etac  conjE i)),
-             tactical ("applying eqvt_simp      ", eqvt_simp_tac_gen_i asm_full_simp_tac tactical ctxt i )]
+      EVERY [tactical ctxt ("unfolding of supports   ", simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps) i),
+             tactical ctxt ("stripping of foralls    ", REPEAT_DETERM (rtac allI i)),
+             tactical ctxt ("geting rid of the imps  ", rtac impI i),
+             tactical ctxt ("eliminating conjuncts   ", REPEAT_DETERM (etac  conjE i)),
+             tactical ctxt ("applying eqvt_simp      ", eqvt_simp_tac_gen_i asm_full_simp_tac tactical ctxt i )]
   end;
 
 
@@ -314,7 +314,7 @@
             val fin_supp = dynamic_thms st ("fin_supp")
             val ctxt' = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
           in
-            (tactical ("guessing of the right supports-set",
+            (tactical ctxt ("guessing of the right supports-set",
                       EVERY [compose_tac (false, supports_rule'', 2) i,
                              asm_full_simp_tac ctxt' (i+1),
                              supports_tac_i tactical ctxt i])) st
@@ -356,7 +356,7 @@
             val supports_fresh_rule'' = Drule.cterm_instantiate
               [(cert (head_of S), cert s')] supports_fresh_rule'
           in
-            (tactical ("guessing of the right set that supports the goal", 
+            (tactical ctxt ("guessing of the right set that supports the goal", 
                       (EVERY [compose_tac (false, supports_fresh_rule'', 3) i,
                              asm_full_simp_tac ctxt1 (i+2),
                              asm_full_simp_tac ctxt2 (i+1), 
@@ -364,25 +364,25 @@
           end
           (* when a term-constructor contains more than one binder, it is useful    *) 
           (* in nominal_primrecs to try whether the goal can be solved by an hammer *)
-        | _ => (tactical ("if it is not of the form _\<sharp>_, then try the simplifier",   
+        | _ => (tactical ctxt ("if it is not of the form _\<sharp>_, then try the simplifier",   
                           (asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps [fresh_prod]@fresh_atm) i))) st
     end
     handle General.Subscript => Seq.empty;
 (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
 
-val eqvt_simp_tac        = eqvt_asm_full_simp_tac_i NO_DEBUG_tac;
+val eqvt_simp_tac        = eqvt_asm_full_simp_tac_i NO_DEBUG;
 
-val perm_simp_tac        = perm_asm_full_simp_tac_i NO_DEBUG_tac;
-val perm_extend_simp_tac = perm_extend_simp_tac_i NO_DEBUG_tac;
-val supports_tac         = supports_tac_i NO_DEBUG_tac;
-val finite_guess_tac     = finite_guess_tac_i NO_DEBUG_tac;
-val fresh_guess_tac      = fresh_guess_tac_i NO_DEBUG_tac;
+val perm_simp_tac        = perm_asm_full_simp_tac_i NO_DEBUG;
+val perm_extend_simp_tac = perm_extend_simp_tac_i NO_DEBUG;
+val supports_tac         = supports_tac_i NO_DEBUG;
+val finite_guess_tac     = finite_guess_tac_i NO_DEBUG;
+val fresh_guess_tac      = fresh_guess_tac_i NO_DEBUG;
 
-val dperm_simp_tac        = perm_asm_full_simp_tac_i DEBUG_tac;
-val dperm_extend_simp_tac = perm_extend_simp_tac_i DEBUG_tac;
-val dsupports_tac         = supports_tac_i DEBUG_tac;
-val dfinite_guess_tac     = finite_guess_tac_i DEBUG_tac;
-val dfresh_guess_tac      = fresh_guess_tac_i DEBUG_tac;
+val dperm_simp_tac        = perm_asm_full_simp_tac_i DEBUG;
+val dperm_extend_simp_tac = perm_extend_simp_tac_i DEBUG;
+val dsupports_tac         = supports_tac_i DEBUG;
+val dfinite_guess_tac     = finite_guess_tac_i DEBUG;
+val dfresh_guess_tac      = fresh_guess_tac_i DEBUG;
 
 (* Code opied from the Simplifer for setting up the perm_simp method   *)
 (* behaves nearly identical to the simp-method, for example can handle *)
@@ -393,11 +393,11 @@
 val asm_lrN = "asm_lr";
 
 val perm_simp_options =
- (Args.parens (Args.$$$ no_asmN) >> K (perm_simp_tac_i NO_DEBUG_tac) ||
-  Args.parens (Args.$$$ no_asm_simpN) >> K (perm_asm_simp_tac_i NO_DEBUG_tac) ||
-  Args.parens (Args.$$$ no_asm_useN) >> K (perm_full_simp_tac_i NO_DEBUG_tac) ||
-  Args.parens (Args.$$$ asm_lrN) >> K (perm_asm_lr_simp_tac_i NO_DEBUG_tac) ||
-  Scan.succeed (perm_asm_full_simp_tac_i NO_DEBUG_tac));
+ (Args.parens (Args.$$$ no_asmN) >> K (perm_simp_tac_i NO_DEBUG) ||
+  Args.parens (Args.$$$ no_asm_simpN) >> K (perm_asm_simp_tac_i NO_DEBUG) ||
+  Args.parens (Args.$$$ no_asm_useN) >> K (perm_full_simp_tac_i NO_DEBUG) ||
+  Args.parens (Args.$$$ asm_lrN) >> K (perm_asm_lr_simp_tac_i NO_DEBUG) ||
+  Scan.succeed (perm_asm_full_simp_tac_i NO_DEBUG));
 
 val perm_simp_meth =
   Scan.lift perm_simp_options --| Method.sections (Simplifier.simp_modifiers') >>
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/HOL/Nominal/nominal_thmdecls.ML
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Thu Apr 10 14:40:11 2014 +0200
@@ -47,7 +47,7 @@
 
 fun tactic ctxt (msg, tac) =
   if Config.get ctxt nominal_eqvt_debug
-  then tac THEN' (K (print_tac ("after " ^ msg)))
+  then tac THEN' (K (print_tac ctxt ("after " ^ msg)))
   else tac
 
 fun prove_eqvt_tac ctxt orig_thm pi pi' =
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/Orderings.thy	Thu Apr 10 14:40:11 2014 +0200
@@ -344,21 +344,19 @@
 subsection {* Reasoning tools setup *}
 
 ML {*
-
 signature ORDERS =
 sig
   val print_structures: Proof.context -> unit
-  val attrib_setup: theory -> theory
   val order_tac: Proof.context -> thm list -> int -> tactic
 end;
 
 structure Orders: ORDERS =
 struct
 
-(** Theory and context data **)
+(* context data *)
 
 fun struct_eq ((s1: string, ts1), (s2, ts2)) =
-  (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
+  s1 = s2 andalso eq_list (op aconv) (ts1, ts2);
 
 structure Data = Generic_Data
 (
@@ -386,44 +384,52 @@
     Pretty.writeln (Pretty.big_list "order structures:" (map pretty_struct structs))
   end;
 
-
-(** Method **)
+val _ =
+  Outer_Syntax.improper_command @{command_spec "print_orders"}
+    "print order structures available to transitivity reasoner"
+    (Scan.succeed (Toplevel.unknown_context o
+      Toplevel.keep (print_structures o Toplevel.context_of)));
 
-fun struct_tac ((s, [eq, le, less]), thms) ctxt prems =
+
+(* tactics *)
+
+fun struct_tac ((s, ops), thms) ctxt facts =
   let
+    val [eq, le, less] = ops;
     fun decomp thy (@{const Trueprop} $ t) =
-      let
-        fun excluded t =
-          (* exclude numeric types: linear arithmetic subsumes transitivity *)
-          let val T = type_of t
-          in
-            T = HOLogic.natT orelse T = HOLogic.intT orelse T = HOLogic.realT
-          end;
-        fun rel (bin_op $ t1 $ t2) =
-              if excluded t1 then NONE
-              else if Pattern.matches thy (eq, bin_op) then SOME (t1, "=", t2)
-              else if Pattern.matches thy (le, bin_op) then SOME (t1, "<=", t2)
-              else if Pattern.matches thy (less, bin_op) then SOME (t1, "<", t2)
-              else NONE
-          | rel _ = NONE;
-        fun dec (Const (@{const_name Not}, _) $ t) = (case rel t
-              of NONE => NONE
-               | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
-          | dec x = rel x;
-      in dec t end
-      | decomp thy _ = NONE;
+          let
+            fun excluded t =
+              (* exclude numeric types: linear arithmetic subsumes transitivity *)
+              let val T = type_of t
+              in
+                T = HOLogic.natT orelse T = HOLogic.intT orelse T = HOLogic.realT
+              end;
+            fun rel (bin_op $ t1 $ t2) =
+                  if excluded t1 then NONE
+                  else if Pattern.matches thy (eq, bin_op) then SOME (t1, "=", t2)
+                  else if Pattern.matches thy (le, bin_op) then SOME (t1, "<=", t2)
+                  else if Pattern.matches thy (less, bin_op) then SOME (t1, "<", t2)
+                  else NONE
+              | rel _ = NONE;
+            fun dec (Const (@{const_name Not}, _) $ t) =
+                  (case rel t of NONE =>
+                    NONE
+                  | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
+              | dec x = rel x;
+          in dec t end
+      | decomp _ _ = NONE;
   in
-    case s of
-      "order" => Order_Tac.partial_tac decomp thms ctxt prems
-    | "linorder" => Order_Tac.linear_tac decomp thms ctxt prems
-    | _ => error ("Unknown kind of order `" ^ s ^ "' encountered in transitivity reasoner.")
+    (case s of
+      "order" => Order_Tac.partial_tac decomp thms ctxt facts
+    | "linorder" => Order_Tac.linear_tac decomp thms ctxt facts
+    | _ => error ("Unknown order kind " ^ quote s ^ " encountered in transitivity reasoner"))
   end
 
-fun order_tac ctxt prems =
-  FIRST' (map (fn s => CHANGED o struct_tac s ctxt prems) (Data.get (Context.Proof ctxt)));
+fun order_tac ctxt facts =
+  FIRST' (map (fn s => CHANGED o struct_tac s ctxt facts) (Data.get (Context.Proof ctxt)));
 
 
-(** Attribute **)
+(* attributes *)
 
 fun add_struct_thm s tag =
   Thm.declaration_attribute
@@ -432,30 +438,19 @@
   Thm.declaration_attribute
     (fn _ => Data.map (AList.delete struct_eq s));
 
-val attrib_setup =
-  Attrib.setup @{binding order}
-    (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
-      Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
-      Scan.repeat Args.term
-      >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
-           | ((NONE, n), ts) => del_struct (n, ts)))
-    "theorems controlling transitivity reasoner";
-
-
-(** Diagnostic command **)
-
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_orders"}
-    "print order structures available to transitivity reasoner"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (print_structures o Toplevel.context_of)));
+  Theory.setup
+    (Attrib.setup @{binding order}
+      (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
+        Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
+        Scan.repeat Args.term
+        >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
+             | ((NONE, n), ts) => del_struct (n, ts)))
+      "theorems controlling transitivity reasoner");
 
 end;
-
 *}
 
-setup Orders.attrib_setup
-
 method_setup order = {*
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (Orders.order_tac ctxt []))
 *} "transitivity reasoner"
@@ -546,64 +541,64 @@
 
 end
 
-
 setup {*
-let
-
-fun prp t thm = Thm.prop_of thm = t;  (* FIXME aconv!? *)
+  map_theory_simpset (fn ctxt0 => ctxt0 addSolver
+    mk_solver "Transitivity" (fn ctxt => Orders.order_tac ctxt (Simplifier.prems_of ctxt)))
+  (*Adding the transitivity reasoners also as safe solvers showed a slight
+    speed up, but the reasoning strength appears to be not higher (at least
+    no breaking of additional proofs in the entire HOL distribution, as
+    of 5 March 2004, was observed).*)
+*}
 
-fun prove_antisym_le ctxt ((le as Const(_,T)) $ r $ s) =
-  let val prems = Simplifier.prems_of ctxt;
-      val less = Const (@{const_name less}, T);
-      val t = HOLogic.mk_Trueprop(le $ s $ r);
-  in case find_first (prp t) prems of
-       NONE =>
-         let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s))
-         in case find_first (prp t) prems of
-              NONE => NONE
-            | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv1}))
-         end
-     | SOME thm => SOME(mk_meta_eq(thm RS @{thm order_class.antisym_conv}))
-  end
-  handle THM _ => NONE;
+ML {*
+local
+  fun prp t thm = Thm.prop_of thm = t;  (* FIXME proper aconv!? *)
+in
 
-fun prove_antisym_less ctxt (NotC $ ((less as Const(_,T)) $ r $ s)) =
-  let val prems = Simplifier.prems_of ctxt;
-      val le = Const (@{const_name less_eq}, T);
-      val t = HOLogic.mk_Trueprop(le $ r $ s);
-  in case find_first (prp t) prems of
-       NONE =>
-         let val t = HOLogic.mk_Trueprop(NotC $ (less $ s $ r))
-         in case find_first (prp t) prems of
-              NONE => NONE
-            | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3}))
-         end
-     | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv2}))
-  end
-  handle THM _ => NONE;
+fun antisym_le_simproc ctxt ct =
+  (case term_of ct of
+    (le as Const (_, T)) $ r $ s =>
+     (let
+        val prems = Simplifier.prems_of ctxt;
+        val less = Const (@{const_name less}, T);
+        val t = HOLogic.mk_Trueprop(le $ s $ r);
+      in
+        (case find_first (prp t) prems of
+          NONE =>
+            let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s)) in
+              (case find_first (prp t) prems of
+                NONE => NONE
+              | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv1})))
+             end
+         | SOME thm => SOME (mk_meta_eq (thm RS @{thm order_class.antisym_conv})))
+      end handle THM _ => NONE)
+  | _ => NONE);
 
-fun add_simprocs procs thy =
-  map_theory_simpset (fn ctxt => ctxt
-    addsimprocs (map (fn (name, raw_ts, proc) =>
-      Simplifier.simproc_global thy name raw_ts proc) procs)) thy;
-
-fun add_solver name tac =
-  map_theory_simpset (fn ctxt0 => ctxt0 addSolver
-    mk_solver name (fn ctxt => tac ctxt (Simplifier.prems_of ctxt)));
+fun antisym_less_simproc ctxt ct =
+  (case term_of ct of
+    NotC $ ((less as Const(_,T)) $ r $ s) =>
+     (let
+       val prems = Simplifier.prems_of ctxt;
+       val le = Const (@{const_name less_eq}, T);
+       val t = HOLogic.mk_Trueprop(le $ r $ s);
+      in
+        (case find_first (prp t) prems of
+          NONE =>
+            let val t = HOLogic.mk_Trueprop (NotC $ (less $ s $ r)) in
+              (case find_first (prp t) prems of
+                NONE => NONE
+              | SOME thm => SOME (mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3})))
+            end
+        | SOME thm => SOME (mk_meta_eq (thm RS @{thm linorder_class.antisym_conv2})))
+      end handle THM _ => NONE)
+  | _ => NONE);
 
-in
-  add_simprocs [
-       ("antisym le", ["(x::'a::order) <= y"], prove_antisym_le),
-       ("antisym less", ["~ (x::'a::linorder) < y"], prove_antisym_less)
-     ]
-  #> add_solver "Transitivity" Orders.order_tac
-  (* Adding the transitivity reasoners also as safe solvers showed a slight
-     speed up, but the reasoning strength appears to be not higher (at least
-     no breaking of additional proofs in the entire HOL distribution, as
-     of 5 March 2004, was observed). *)
-end
+end;
 *}
 
+simproc_setup antisym_le ("(x::'a::order) \<le> y") = "K antisym_le_simproc"
+simproc_setup antisym_less ("\<not> (x::'a::linorder) < y") = "K antisym_less_simproc"
+
 
 subsection {* Bounded quantifiers *}
 
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/HOL/Probability/measurable.ML
--- a/src/HOL/Probability/measurable.ML	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/Probability/measurable.ML	Thu Apr 10 14:40:11 2014 +0200
@@ -95,7 +95,7 @@
 
 fun add_thm (raw, lv) thm ctxt = add (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
 
-fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac (msg ()) THEN f else f
+fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f
 
 fun nth_hol_goal thm i =
   HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1))))
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/Product_Type.thy	Thu Apr 10 14:40:11 2014 +0200
@@ -1219,8 +1219,37 @@
 
 subsection {* Inductively defined sets *}
 
+(* simplify {(x1, ..., xn). (x1, ..., xn) : S} to S *)
+simproc_setup Collect_mem ("Collect t") = {*
+  fn _ => fn ctxt => fn ct =>
+    (case term_of ct of
+      S as Const (@{const_name Collect}, Type (@{type_name fun}, [_, T])) $ t =>
+        let val (u, _, ps) = HOLogic.strip_psplits t in
+          (case u of
+            (c as Const (@{const_name Set.member}, _)) $ q $ S' =>
+              (case try (HOLogic.strip_ptuple ps) q of
+                NONE => NONE
+              | SOME ts =>
+                  if not (Term.is_open S') andalso
+                    ts = map Bound (length ps downto 0)
+                  then
+                    let val simp =
+                      full_simp_tac (put_simpset HOL_basic_ss ctxt
+                        addsimps [@{thm split_paired_all}, @{thm split_conv}]) 1
+                    in
+                      SOME (Goal.prove ctxt [] []
+                        (Const (@{const_name Pure.eq}, T --> T --> propT) $ S $ S')
+                        (K (EVERY
+                          [rtac eq_reflection 1, rtac @{thm subset_antisym} 1,
+                           rtac subsetI 1, dtac CollectD 1, simp,
+                           rtac subsetI 1, rtac CollectI 1, simp])))
+                    end
+                  else NONE)
+          | _ => NONE)
+        end
+    | _ => NONE)
+*}
 ML_file "Tools/inductive_set.ML"
-setup Inductive_Set.setup
 
 
 subsection {* Legacy theorem bindings and duplicates *}
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Thu Apr 10 14:40:11 2014 +0200
@@ -25,20 +25,11 @@
 
 (* debug stuff *)
 
-fun print_tac options s = 
-  if show_proof_trace options then Tactical.print_tac s else Seq.single;
-
-
-(** auxiliary **)
+fun trace_tac ctxt options s =
+  if show_proof_trace options then print_tac ctxt s else Seq.single;
 
-datatype assertion = Max_number_of_subgoals of int
-
-fun assert_tac (Max_number_of_subgoals i) st =
-  if (nprems_of st <= i) then Seq.single st
-  else
-    raise Fail ("assert_tac: Numbers of subgoals mismatch at goal state :\n" ^
-      Pretty.string_of (Pretty.chunks
-        (Goal_Display.pretty_goals_without_context st)))
+fun assert_tac ctxt pos pred =
+  COND pred all_tac (print_tac ctxt ("Assertion failed" ^ Position.here pos) THEN no_tac);
 
 
 (** special setup for simpset **)
@@ -75,7 +66,7 @@
            @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
            @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
       | Free _ =>
-        Subgoal.FOCUS_PREMS (fn {context = ctxt', params = params, prems, asms, concl, schematics} =>
+        Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, ...} =>
           let
             val prems' = maps dest_conjunct_prem (take nargs prems)
           in
@@ -84,9 +75,9 @@
       | Abs _ => raise Fail "prove_param: No valid parameter term")
   in
     REPEAT_DETERM (rtac @{thm ext} 1)
-    THEN print_tac options "prove_param"
-    THEN f_tac 
-    THEN print_tac options "after prove_param"
+    THEN trace_tac ctxt options "prove_param"
+    THEN f_tac
+    THEN trace_tac ctxt options "after prove_param"
     THEN (REPEAT_DETERM (atac 1))
     THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
     THEN REPEAT_DETERM (rtac @{thm refl} 1)
@@ -101,20 +92,20 @@
         val param_derivations = param_derivations_of deriv
         val ho_args = ho_args_of mode args
       in
-        print_tac options "before intro rule:"
+        trace_tac ctxt options "before intro rule:"
         THEN rtac introrule 1
-        THEN print_tac options "after intro rule"
+        THEN trace_tac ctxt options "after intro rule"
         (* for the right assumption in first position *)
         THEN rotate_tac premposition 1
         THEN atac 1
-        THEN print_tac options "parameter goal"
+        THEN trace_tac ctxt options "parameter goal"
         (* work with parameter arguments *)
         THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
         THEN (REPEAT_DETERM (atac 1))
       end
   | (Free _, _) =>
-      print_tac options "proving parameter call.."
-      THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', params, prems, asms, concl, schematics} =>
+      trace_tac ctxt options "proving parameter call.."
+      THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, concl, ...} =>
           let
             val param_prem = nth prems premposition
             val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem))
@@ -129,14 +120,14 @@
           in
             rtac param_prem' 1
           end) ctxt 1
-      THEN print_tac options "after prove parameter call")
+      THEN trace_tac ctxt options "after prove parameter call")
 
 fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st
 
 fun prove_match options ctxt nargs out_ts =
   let
     val eval_if_P =
-      @{lemma "P ==> Predicate.eval x z ==> Predicate.eval (if P then x else y) z" by simp} 
+      @{lemma "P ==> Predicate.eval x z ==> Predicate.eval (if P then x else y) z" by simp}
     fun get_case_rewrite t =
       if is_constructor ctxt t then
         let
@@ -151,13 +142,13 @@
   in
     (* make this simpset better! *)
     asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps simprules) 1
-    THEN print_tac options "after prove_match:"
-    THEN (DETERM (TRY 
+    THEN trace_tac ctxt options "after prove_match:"
+    THEN (DETERM (TRY
            (rtac eval_if_P 1
-           THEN (SUBPROOF (fn {context, params, prems, asms, concl, schematics} =>
+           THEN (SUBPROOF (fn {prems, ...} =>
              (REPEAT_DETERM (rtac @{thm conjI} 1
              THEN (SOLVED (asm_simp_tac (put_simpset HOL_basic_ss' ctxt) 1))))
-             THEN print_tac options "if condition to be solved:"
+             THEN trace_tac ctxt options "if condition to be solved:"
              THEN asm_simp_tac (put_simpset HOL_basic_ss' ctxt) 1
              THEN TRY (
                 let
@@ -167,8 +158,8 @@
                     (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
                 end
              THEN REPEAT_DETERM (rtac @{thm refl} 1))
-             THEN print_tac options "after if simp; in SUBPROOF") ctxt 1))))
-    THEN print_tac options "after if simplification"
+             THEN trace_tac ctxt options "after if simp; in SUBPROOF") ctxt 1))))
+    THEN trace_tac ctxt options "after if simplification"
   end;
 
 
@@ -187,7 +178,7 @@
       (fn (pred, T) => predfun_definition_of ctxt pred
         (all_input_of T))
         preds
-  in 
+  in
     simp_tac (put_simpset HOL_basic_ss ctxt
       addsimps (@{thms HOL.simp_thms eval_pred} @ defs)) 1
     (* need better control here! *)
@@ -198,11 +189,11 @@
     val (in_ts, clause_out_ts) = split_mode mode ts;
     fun prove_prems out_ts [] =
         (prove_match options ctxt nargs out_ts)
-        THEN print_tac options "before simplifying assumptions"
+        THEN trace_tac ctxt options "before simplifying assumptions"
         THEN asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1
-        THEN print_tac options "before single intro rule"
+        THEN trace_tac ctxt options "before single intro rule"
         THEN Subgoal.FOCUS_PREMS
-           (fn {context = ctxt', params, prems, asms, concl, schematics} =>
+           (fn {context = ctxt', prems, ...} =>
             let
               val prems' = maps dest_conjunct_prem (take nargs prems)
             in
@@ -221,11 +212,11 @@
                 val (_, out_ts''') = split_mode mode us
                 val rec_tac = prove_prems out_ts''' ps
               in
-                print_tac options "before clause:"
+                trace_tac ctxt options "before clause:"
                 (*THEN asm_simp_tac (put_simpset HOL_basic_ss ctxt) 1*)
-                THEN print_tac options "before prove_expr:"
+                THEN trace_tac ctxt options "before prove_expr:"
                 THEN prove_expr options ctxt nargs premposition (t, deriv)
-                THEN print_tac options "after prove_expr:"
+                THEN trace_tac ctxt options "after prove_expr:"
                 THEN rec_tac
               end
             | Negprem t =>
@@ -240,17 +231,16 @@
                 val param_derivations = param_derivations_of deriv
                 val params = ho_args_of mode args
               in
-                print_tac options "before prove_neg_expr:"
+                trace_tac ctxt options "before prove_neg_expr:"
                 THEN full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
                   [@{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
                    @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
                 THEN (if (is_some name) then
-                    print_tac options "before applying not introduction rule"
-                    THEN Subgoal.FOCUS_PREMS
-                      (fn {context, params = params, prems, asms, concl, schematics} =>
-                        rtac (the neg_intro_rule) 1
-                        THEN rtac (nth prems premposition) 1) ctxt 1
-                    THEN print_tac options "after applying not introduction rule"
+                    trace_tac ctxt options "before applying not introduction rule"
+                    THEN Subgoal.FOCUS_PREMS (fn {prems, ...} =>
+                      rtac (the neg_intro_rule) 1
+                      THEN rtac (nth prems premposition) 1) ctxt 1
+                    THEN trace_tac ctxt options "after applying not introduction rule"
                     THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations))
                     THEN (REPEAT_DETERM (atac 1))
                   else
@@ -265,16 +255,16 @@
               end
             | Sidecond t =>
              rtac @{thm if_predI} 1
-             THEN print_tac options "before sidecond:"
+             THEN trace_tac ctxt options "before sidecond:"
              THEN prove_sidecond ctxt t
-             THEN print_tac options "after sidecond:"
+             THEN trace_tac ctxt options "after sidecond:"
              THEN prove_prems [] ps)
         in (prove_match options ctxt nargs out_ts)
             THEN rest_tac
         end
     val prems_tac = prove_prems in_ts moded_ps
   in
-    print_tac options "Proving clause..."
+    trace_tac ctxt options "Proving clause..."
     THEN rtac @{thm bindI} 1
     THEN rtac @{thm singleI} 1
     THEN prems_tac
@@ -291,15 +281,15 @@
     val pred_case_rule = the_elim_of ctxt pred
   in
     REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all}))
-    THEN print_tac options "before applying elim rule"
+    THEN trace_tac ctxt options "before applying elim rule"
     THEN etac (predfun_elim_of ctxt pred mode) 1
     THEN etac pred_case_rule 1
-    THEN print_tac options "after applying elim rule"
+    THEN trace_tac ctxt options "after applying elim rule"
     THEN (EVERY (map
-           (fn i => EVERY' (select_sup (length moded_clauses) i) i) 
+           (fn i => EVERY' (select_sup (length moded_clauses) i) i)
              (1 upto (length moded_clauses))))
     THEN (EVERY (map2 (prove_clause options ctxt nargs mode) clauses moded_clauses))
-    THEN print_tac options "proved one direction"
+    THEN trace_tac ctxt options "proved one direction"
   end
 
 
@@ -316,15 +306,15 @@
             val num_of_constrs = length case_thms
             val (_, ts) = strip_comb t
           in
-            print_tac options ("Term " ^ (Syntax.string_of_term ctxt t) ^ 
+            trace_tac ctxt options ("Term " ^ (Syntax.string_of_term ctxt t) ^
               " splitting with rules \n" ^ Display.string_of_thm ctxt split_asm)
             THEN TRY (Splitter.split_asm_tac [split_asm] 1
-              THEN (print_tac options "after splitting with split_asm rules")
+              THEN (trace_tac ctxt options "after splitting with split_asm rules")
             (* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1)
               THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
               THEN (REPEAT_DETERM_N (num_of_constrs - 1)
                 (etac @{thm botE} 1 ORELSE etac @{thm botE} 2)))
-            THEN (assert_tac (Max_number_of_subgoals 2))
+            THEN assert_tac ctxt @{here} (fn st => Thm.nprems_of st <= 2)
             THEN (EVERY (map split_term_tac ts))
           end
       else all_tac
@@ -334,7 +324,7 @@
     THEN (etac @{thm botE} 2))))
   end
 
-(* VERY LARGE SIMILIRATIY to function prove_param 
+(* VERY LARGE SIMILIRATIY to function prove_param
 -- join both functions
 *)
 (* TODO: remove function *)
@@ -347,19 +337,19 @@
     val ho_args = ho_args_of mode args
     val f_tac =
       (case f of
-        Const (name, _) => full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps 
+        Const (name, _) => full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
            (@{thm eval_pred}::(predfun_definition_of ctxt name mode)
            :: @{thm "Product_Type.split_conv"}::[])) 1
       | Free _ => all_tac
       | _ => error "prove_param2: illegal parameter term")
   in
-    print_tac options "before simplification in prove_args:"
+    trace_tac ctxt options "before simplification in prove_args:"
     THEN f_tac
-    THEN print_tac options "after simplification in prove_args"
+    THEN trace_tac ctxt options "after simplification in prove_args"
     THEN EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations)
   end
 
-fun prove_expr2 options ctxt (t, deriv) = 
+fun prove_expr2 options ctxt (t, deriv) =
   (case strip_comb t of
       (Const (name, _), args) =>
         let
@@ -369,11 +359,11 @@
         in
           etac @{thm bindE} 1
           THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
-          THEN print_tac options "prove_expr2-before"
+          THEN trace_tac ctxt options "prove_expr2-before"
           THEN etac (predfun_elim_of ctxt name mode) 1
-          THEN print_tac options "prove_expr2"
+          THEN trace_tac ctxt options "prove_expr2"
           THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
-          THEN print_tac options "finished prove_expr2"
+          THEN trace_tac ctxt options "finished prove_expr2"
         end
       | _ => etac @{thm bindE} 1)
 
@@ -387,16 +377,16 @@
       | _ => nameTs)
     val preds = preds_of t []
     val defs = map
-      (fn (pred, T) => predfun_definition_of ctxt pred 
+      (fn (pred, T) => predfun_definition_of ctxt pred
         (all_input_of T))
         preds
   in
     (* only simplify the one assumption *)
-    full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm eval_pred} :: defs) 1 
+    full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm eval_pred} :: defs) 1
     (* need better control here! *)
-    THEN print_tac options "after sidecond2 simplification"
+    THEN trace_tac ctxt options "after sidecond2 simplification"
   end
-  
+
 fun prove_clause2 options ctxt pred mode (ts, ps) i =
   let
     val pred_intro_rule = nth (intros_of ctxt pred) (i - 1)
@@ -406,23 +396,23 @@
       addsimps [@{thm split_eta}, @{thm split_beta},
         @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
     fun prove_prems2 out_ts [] =
-      print_tac options "before prove_match2 - last call:"
+      trace_tac ctxt options "before prove_match2 - last call:"
       THEN prove_match2 options ctxt out_ts
-      THEN print_tac options "after prove_match2 - last call:"
+      THEN trace_tac ctxt options "after prove_match2 - last call:"
       THEN (etac @{thm singleE} 1)
       THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
       THEN (asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1)
       THEN TRY (
         (REPEAT_DETERM (etac @{thm Pair_inject} 1))
         THEN (asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1)
-        
-        THEN SOLVED (print_tac options "state before applying intro rule:"
+
+        THEN SOLVED (trace_tac ctxt options "state before applying intro rule:"
         THEN (rtac pred_intro_rule
         (* How to handle equality correctly? *)
-        THEN_ALL_NEW (K (print_tac options "state before assumption matching")
+        THEN_ALL_NEW (K (trace_tac ctxt options "state before assumption matching")
         THEN' (atac ORELSE' ((CHANGED o asm_full_simp_tac split_simpset) THEN' (TRY o atac)))
-          THEN' (K (print_tac options "state after pre-simplification:"))
-        THEN' (K (print_tac options "state after assumption matching:")))) 1))
+          THEN' (K (trace_tac ctxt options "state after pre-simplification:"))
+        THEN' (K (trace_tac ctxt options "state after assumption matching:")))) 1))
     | prove_prems2 out_ts ((p, deriv) :: ps) =
       let
         val mode = head_mode_of deriv
@@ -445,7 +435,7 @@
                 val param_derivations = param_derivations_of deriv
                 val ho_args = ho_args_of mode args
               in
-                print_tac options "before neg prem 2"
+                trace_tac ctxt options "before neg prem 2"
                 THEN etac @{thm bindE} 1
                 THEN (if is_some name then
                     full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
@@ -456,28 +446,28 @@
                   else
                     etac @{thm not_predE'} 1)
                 THEN rec_tac
-              end 
+              end
           | Sidecond t =>
               etac @{thm bindE} 1
               THEN etac @{thm if_predE} 1
               THEN prove_sidecond2 options ctxt t
               THEN prove_prems2 [] ps)
       in
-        print_tac options "before prove_match2:"
+        trace_tac ctxt options "before prove_match2:"
         THEN prove_match2 options ctxt out_ts
-        THEN print_tac options "after prove_match2:"
+        THEN trace_tac ctxt options "after prove_match2:"
         THEN rest_tac
       end
-    val prems_tac = prove_prems2 in_ts ps 
+    val prems_tac = prove_prems2 in_ts ps
   in
-    print_tac options "starting prove_clause2"
+    trace_tac ctxt options "starting prove_clause2"
     THEN etac @{thm bindE} 1
     THEN (etac @{thm singleE'} 1)
     THEN (TRY (etac @{thm Pair_inject} 1))
-    THEN print_tac options "after singleE':"
+    THEN trace_tac ctxt options "after singleE':"
     THEN prems_tac
   end;
- 
+
 fun prove_other_direction options ctxt pred mode moded_clauses =
   let
     fun prove_clause clause i =
@@ -505,11 +495,11 @@
       (if not (skip_proof options) then
         (fn _ =>
         rtac @{thm pred_iffI} 1
-        THEN print_tac options "after pred_iffI"
+        THEN trace_tac ctxt options "after pred_iffI"
         THEN prove_one_direction options ctxt clauses preds pred mode moded_clauses
-        THEN print_tac options "proved one direction"
+        THEN trace_tac ctxt options "proved one direction"
         THEN prove_other_direction options ctxt pred mode moded_clauses
-        THEN print_tac options "proved other direction")
+        THEN trace_tac ctxt options "proved other direction")
       else (fn _ => ALLGOALS Skip_Proof.cheat_tac))
   end
 
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/HOL/Tools/cnf.ML
--- a/src/HOL/Tools/cnf.ML	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/Tools/cnf.ML	Thu Apr 10 14:40:11 2014 +0200
@@ -207,9 +207,9 @@
       in
         make_nnf_iff OF [thm1, thm2, thm3, thm4]
       end
-  | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name False}, _)) =
+  | make_nnf_thm _ (Const (@{const_name Not}, _) $ Const (@{const_name False}, _)) =
       make_nnf_not_false
-  | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
+  | make_nnf_thm _ (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
       make_nnf_not_true
   | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.conj}, _) $ x $ y)) =
       let
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Thu Apr 10 14:40:11 2014 +0200
@@ -25,42 +25,11 @@
   val mono_add: attribute
   val mono_del: attribute
   val codegen_preproc: theory -> thm list -> thm list
-  val setup: theory -> theory
 end;
 
 structure Inductive_Set: INDUCTIVE_SET =
 struct
 
-(**** simplify {(x1, ..., xn). (x1, ..., xn) : S} to S ****)
-
-val collect_mem_simproc =
-  Simplifier.simproc_global @{theory Set} "Collect_mem" ["Collect t"] (fn ctxt =>
-    fn S as Const (@{const_name Collect}, Type ("fun", [_, T])) $ t =>
-         let val (u, _, ps) = HOLogic.strip_psplits t
-         in case u of
-           (c as Const (@{const_name Set.member}, _)) $ q $ S' =>
-             (case try (HOLogic.strip_ptuple ps) q of
-                NONE => NONE
-              | SOME ts =>
-                  if not (Term.is_open S') andalso
-                    ts = map Bound (length ps downto 0)
-                  then
-                    let val simp =
-                      full_simp_tac (put_simpset HOL_basic_ss ctxt
-                        addsimps [@{thm split_paired_all}, @{thm split_conv}]) 1
-                    in
-                      SOME (Goal.prove ctxt [] []
-                        (Const (@{const_name Pure.eq}, T --> T --> propT) $ S $ S')
-                        (K (EVERY
-                          [rtac eq_reflection 1, rtac @{thm subset_antisym} 1,
-                           rtac subsetI 1, dtac CollectD 1, simp,
-                           rtac subsetI 1, rtac CollectI 1, simp])))
-                    end
-                  else NONE)
-         | _ => NONE
-         end
-     | _ => NONE);
-
 (***********************************************************************************)
 (* simplifies (%x y. (x, y) : S & P x y) to (%x y. (x, y) : S Int {(x, y). P x y}) *)
 (* and        (%x y. (x, y) : S | P x y) to (%x y. (x, y) : S Un {(x, y). P x y})  *)
@@ -206,7 +175,7 @@
   (swap #> Pattern.matches thy) (f #> fst) (op aconv) rules;
 
 fun infer_arities thy arities (optf, t) fs = case strip_comb t of
-    (Abs (s, T, u), []) => infer_arities thy arities (NONE, u) fs
+    (Abs (_, _, u), []) => infer_arities thy arities (NONE, u) fs
   | (Abs _, _) => infer_arities thy arities (NONE, Envir.beta_norm t) fs
   | (u, ts) => (case Option.map (lookup_arity thy arities) (name_type_of u) of
       SOME (SOME (_, (arity, _))) =>
@@ -266,7 +235,7 @@
           end)
   in
     Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm split_conv}]
-      addsimprocs [collect_mem_simproc]) thm'' |>
+      addsimprocs [@{simproc Collect_mem}]) thm'' |>
         zero_var_indexes |> eta_contract_thm (equal p)
   end;
 
@@ -397,7 +366,7 @@
     thm |>
     Thm.instantiate ([], insts) |>
     Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps to_set_simps
-        addsimprocs [strong_ind_simproc pred_arities, collect_mem_simproc]) |>
+        addsimprocs [strong_ind_simproc pred_arities, @{simproc Collect_mem}]) |>
     Rule_Cases.save thm
   end;
 
@@ -425,8 +394,6 @@
       else thm
   in map preproc end;
 
-fun code_ind_att optmod = to_pred_att [];
-
 
 (**** definition of inductive sets ****)
 
@@ -569,21 +536,21 @@
 
 (** package setup **)
 
-(* setup theory *)
+(* attributes *)
 
-val setup =
-  Attrib.setup @{binding pred_set_conv} (Scan.succeed pred_set_conv_att)
-    "declare rules for converting between predicate and set notation" #>
-  Attrib.setup @{binding to_set} (Attrib.thms >> to_set_att)
-    "convert rule to set notation" #>
-  Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att)
-    "convert rule to predicate notation" #>
-  Attrib.setup @{binding mono_set} (Attrib.add_del mono_add mono_del)
-    "declaration of monotonicity rule for set operators" #>
-  map_theory_simpset (fn ctxt => ctxt addsimprocs [collect_mem_simproc]);
+val _ =
+  Theory.setup
+   (Attrib.setup @{binding pred_set_conv} (Scan.succeed pred_set_conv_att)
+      "declare rules for converting between predicate and set notation" #>
+    Attrib.setup @{binding to_set} (Attrib.thms >> to_set_att)
+      "convert rule to set notation" #>
+    Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att)
+      "convert rule to predicate notation" #>
+    Attrib.setup @{binding mono_set} (Attrib.add_del mono_add mono_del)
+      "declare of monotonicity rule for set operators");
 
 
-(* outer syntax *)
+(* commands *)
 
 val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
 
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/Tools/record.ML	Thu Apr 10 14:40:11 2014 +0200
@@ -1066,7 +1066,7 @@
     subrecord.
 *)
 val simproc =
-  Simplifier.simproc_global @{theory HOL} "record_simp" ["x"]
+  Simplifier.simproc_global @{theory HOL} "record" ["x"]
     (fn ctxt => fn t =>
       let val thy = Proof_Context.theory_of ctxt in
         (case t of
@@ -1142,7 +1142,7 @@
   we omit considering further updates if doing so would introduce
   both a more update and an update to a field within it.*)
 val upd_simproc =
-  Simplifier.simproc_global @{theory HOL} "record_upd_simp" ["x"]
+  Simplifier.simproc_global @{theory HOL} "record_upd" ["x"]
     (fn ctxt => fn t =>
       let
         val thy = Proof_Context.theory_of ctxt;
@@ -1263,7 +1263,7 @@
  Complexity: #components * #updates     #updates
 *)
 val eq_simproc =
-  Simplifier.simproc_global @{theory HOL} "record_eq_simp" ["r = s"]
+  Simplifier.simproc_global @{theory HOL} "record_eq" ["r = s"]
     (fn ctxt => fn t =>
       (case t of Const (@{const_name HOL.eq}, Type (_, [T, _])) $ _ $ _ =>
         (case rec_id ~1 T of
@@ -1283,7 +1283,7 @@
     P t = ~1: completely split
     P t > 0: split up to given bound of record extensions.*)
 fun split_simproc P =
-  Simplifier.simproc_global @{theory HOL} "record_split_simp" ["x"]
+  Simplifier.simproc_global @{theory HOL} "record_split" ["x"]
     (fn ctxt => fn t =>
       (case t of
         Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
@@ -1311,7 +1311,7 @@
       | _ => NONE));
 
 val ex_sel_eq_simproc =
-  Simplifier.simproc_global @{theory HOL} "ex_sel_eq_simproc" ["Ex t"]
+  Simplifier.simproc_global @{theory HOL} "ex_sel_eq" ["Ex t"]
     (fn ctxt => fn t =>
       let
         val thy = Proof_Context.theory_of ctxt;
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy	Thu Apr 10 14:40:11 2014 +0200
@@ -7,6 +7,32 @@
   "text_cartouche" :: thy_decl
 begin
 
+subsection {* Regular outer syntax *}
+
+text \<open>Text cartouches may be used in the outer syntax category "text",
+  as alternative to the traditional "verbatim" tokens.  An example is
+  this text block.\<close>  -- \<open>The same works for small side-comments.\<close>
+
+notepad
+begin
+  txt \<open>Moreover, cartouches work as additional syntax in the
+    "altstring" category, for literal fact references.  For example:\<close>
+
+  fix x y :: 'a
+  assume "x = y"
+  note \<open>x = y\<close>
+  have "x = y" by (rule \<open>x = y\<close>)
+  from \<open>x = y\<close> have "x = y" .
+
+  txt \<open>Of course, this can be nested inside formal comments and
+    antiquotations, e.g. like this @{thm \<open>x = y\<close>} or this @{thm sym
+    [OF \<open>x = y\<close>]}.\<close>
+
+  have "x = y"
+    by (tactic \<open>rtac @{thm \<open>x = y\<close>} 1\<close>)  -- \<open>more cartouches involving ML\<close>
+end
+
+
 subsection {* Outer syntax: cartouche within command syntax *}
 
 ML {*
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Pure/General/url.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/url.scala	Thu Apr 10 14:40:11 2014 +0200
@@ -0,0 +1,36 @@
+/*  Title:      Pure/General/url.scala
+    Author:     Makarius
+
+Basic URL operations.
+*/
+
+package isabelle
+
+
+import java.net.{URL, MalformedURLException}
+
+
+object Url
+{
+  def apply(name: String): URL =
+  {
+    try { new URL(name) }
+    catch { case _: MalformedURLException => error("Malformed URL " + quote(name)) }
+  }
+
+  def is_wellformed(name: String): Boolean =
+    try { Url(name); true }
+    catch { case ERROR(_) => false }
+
+  def is_readable(name: String): Boolean =
+    try { Url(name).openStream.close; true }
+    catch { case ERROR(_) => false }
+
+  def read(name: String): String =
+  {
+    val stream = Url(name).openStream
+    try { File.read_stream(stream) }
+    finally { stream.close }
+  }
+}
+
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/Isar/args.ML	Thu Apr 10 14:40:11 2014 +0200
@@ -33,6 +33,8 @@
   val maybe: 'a parser -> 'a option parser
   val cartouche_inner_syntax: string parser
   val cartouche_source_position: Symbol_Pos.source parser
+  val text_source_position: Symbol_Pos.source parser
+  val text: string parser
   val name_inner_syntax: string parser
   val name_source_position: Symbol_Pos.source parser
   val name: string parser
@@ -151,8 +153,8 @@
   (Parse.short_ident || Parse.long_ident || Parse.sym_ident || Parse.term_var ||
     Parse.type_ident || Parse.type_var || Parse.number);
 
-val string = Parse.token (Parse.string || Parse.verbatim);
-val alt_string = Parse.token Parse.alt_string;
+val string = Parse.token Parse.string;
+val alt_string = Parse.token (Parse.alt_string || Parse.cartouche);
 val symbolic = Parse.token (Parse.keyword_with Token.ident_or_symbolic);
 
 fun $$$ x =
@@ -163,7 +165,6 @@
       else Scan.fail
     end);
 
-
 val named = ident || string;
 
 val add = $$$ "add";
@@ -183,6 +184,10 @@
 val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
 val cartouche_source_position = cartouche >> Token.source_position_of;
 
+val text_token = named || Parse.token (Parse.verbatim || Parse.cartouche);
+val text_source_position = text_token >> Token.source_position_of;
+val text = text_token >> Token.content_of;
+
 val name_inner_syntax = named >> Token.inner_syntax_of;
 val name_source_position = named >> Token.source_position_of;
 
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/Isar/method.ML	Thu Apr 10 14:40:11 2014 +0200
@@ -513,9 +513,9 @@
   setup @{binding rotate_tac} (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
     (fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i))))
       "rotate assumptions of goal" #>
-  setup @{binding tactic} (Scan.lift Args.name_source_position >> tactic)
+  setup @{binding tactic} (Scan.lift Args.text_source_position >> tactic)
     "ML tactic as proof method" #>
-  setup @{binding raw_tactic} (Scan.lift Args.name_source_position >> raw_tactic)
+  setup @{binding raw_tactic} (Scan.lift Args.text_source_position >> raw_tactic)
     "ML tactic as raw proof method");
 
 
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/Isar/parse.ML	Thu Apr 10 14:40:11 2014 +0200
@@ -275,7 +275,7 @@
   (short_ident || long_ident || sym_ident || string || number);
 
 val text = group (fn () => "text")
-  (short_ident || long_ident || sym_ident || string || number || verbatim);
+  (short_ident || long_ident || sym_ident || string || number || verbatim || cartouche);
 
 val path = group (fn () => "file name/path specification") name;
 
@@ -386,7 +386,7 @@
 
 val const = inner_syntax (group (fn () => "constant") xname);
 
-val literal_fact = inner_syntax (group (fn () => "literal fact") alt_string);
+val literal_fact = inner_syntax (group (fn () => "literal fact") (alt_string || cartouche));
 
 
 (* patterns *)
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/PIDE/command.ML	Thu Apr 10 14:40:11 2014 +0200
@@ -89,9 +89,17 @@
 type blob =
   (string * (SHA1.digest * string list) option) Exn.result;  (*file node name, digest, lines*)
 
-fun read_file master_dir pos src_path =
+fun read_file_node file_node master_dir pos src_path =
   let
     val _ = Position.report pos Markup.language_path;
+    val _ =
+      (case try Url.explode file_node of
+        NONE => ()
+      | SOME (Url.File _) => ()
+      | _ =>
+         (Position.report pos (Markup.path file_node);
+          error ("Prover cannot load remote file " ^
+            Markup.markup (Markup.path file_node) (quote file_node) ^ Position.here pos)));
     val full_path = File.check_file (File.full_path master_dir src_path);
     val _ = Position.report pos (Markup.path (Path.implode full_path));
     val text = File.read full_path;
@@ -99,6 +107,8 @@
     val digest = SHA1.digest text;
   in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end;
 
+val read_file = read_file_node "";
+
 local
 
 fun blob_file src_path lines digest file_node =
@@ -115,8 +125,9 @@
     [span] => span
       |> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) =>
         let
-          fun make_file src_path (Exn.Res (_, NONE)) =
-                Exn.interruptible_capture (fn () => read_file master_dir pos src_path) ()
+          fun make_file src_path (Exn.Res (file_node, NONE)) =
+                Exn.interruptible_capture (fn () =>
+                  read_file_node file_node master_dir pos src_path) ()
             | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
                (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_node)];
                 Exn.Res (blob_file src_path lines digest file_node))
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Thu Apr 10 14:40:11 2014 +0200
@@ -75,6 +75,8 @@
 
   final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
   {
+    def is_empty: Boolean = rep.isEmpty
+
     def apply(index: Markup_Index): Markup_Tree =
       rep.getOrElse(index, Markup_Tree.empty)
 
@@ -86,11 +88,14 @@
         yield id
 
     def redirect(other_id: Document_ID.Generic): Markups =
-      new Markups(
+    {
+      val rep1 =
         (for {
           (Markup_Index(status, Text.Chunk.Id(id)), markup) <- rep.iterator
           if other_id == id
-        } yield (Markup_Index(status, Text.Chunk.Default), markup)).toMap)
+        } yield (Markup_Index(status, Text.Chunk.Default), markup)).toMap
+      if (rep1.isEmpty) Markups.empty else new Markups(rep1)
+    }
 
     override def hashCode: Int = rep.hashCode
     override def equals(that: Any): Boolean =
@@ -135,9 +140,12 @@
 
     def markup(index: Markup_Index): Markup_Tree = markups(index)
 
-    def redirect(other_command: Command): State =
-      new State(other_command, Nil, Results.empty, markups.redirect(other_command.id))
-
+    def redirect(other_command: Command): Option[State] =
+    {
+      val markups1 = markups.redirect(other_command.id)
+      if (markups1.is_empty) None
+      else Some(new State(other_command, Nil, Results.empty, markups1))
+    }
 
     def eq_content(other: State): Boolean =
       command.source == other.command.source &&
@@ -199,11 +207,7 @@
                         case None => bad(); state
                       }
                     case None =>
-                      chunk_name match {
-                        // FIXME workaround for static positions stemming from batch build
-                        case Text.Chunk.File(name) if name.endsWith(".thy") =>
-                        case _ => bad()
-                      }
+                      // silently ignore excessive reports
                       state
                   }
 
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Apr 10 14:40:11 2014 +0200
@@ -536,9 +536,11 @@
       id == st.command.id ||
       (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
 
-    private def other_id(id: Document_ID.Generic): Option[(Text.Chunk.Id, Text.Chunk)] =
+    private def other_id(id: Document_ID.Generic): Option[(Text.Chunk.Id, Text.Chunk)] = None
+    /* FIXME
       (execs.get(id) orElse commands.get(id)).map(st =>
         ((Text.Chunk.Id(st.command.id), st.command.chunk)))
+    */
 
     private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
       (commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) =>
@@ -688,7 +690,7 @@
           } yield (id, st)).toMap.valuesIterator.toList
         }
         else Nil
-      self.map(_._2) ::: others.map(_.redirect(command))
+      self.map(_._2) ::: others.flatMap(_.redirect(command))
     }
 
     def command_results(version: Version, command: Command): Command.Results =
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/PIDE/editor.scala	Thu Apr 10 14:40:11 2014 +0200
@@ -22,7 +22,10 @@
   def insert_overlay(command: Command, fn: String, args: List[String]): Unit
   def remove_overlay(command: Command, fn: String, args: List[String]): Unit
 
-  abstract class Hyperlink { def follow(context: Context): Unit }
+  abstract class Hyperlink {
+    def external: Boolean
+    def follow(context: Context): Unit
+  }
   def hyperlink_command(
     snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink]
 }
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Thu Apr 10 14:40:11 2014 +0200
@@ -214,9 +214,6 @@
 
   /* specific messages */
 
-  def is_inlined(msg: XML.Tree): Boolean =
-    !(is_result(msg) || is_tracing(msg) || is_state(msg))
-
   def is_result(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.RESULT, _), _) => true
@@ -239,8 +236,14 @@
       case _ => false
     }
 
-  def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE)
-  def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION)
+  def is_warning_markup(msg: XML.Tree, name: String): Boolean =
+    msg match {
+      case XML.Elem(Markup(Markup.WARNING, _),
+        List(XML.Elem(markup, _))) => markup.name == name
+      case XML.Elem(Markup(Markup.WARNING_MESSAGE, _),
+        List(XML.Elem(markup, _))) => markup.name == name
+      case _ => false
+    }
 
   def is_warning(msg: XML.Tree): Boolean =
     msg match {
@@ -256,6 +259,13 @@
       case _ => false
     }
 
+  def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE)
+  def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION)
+  def is_legacy(msg: XML.Tree): Boolean = is_warning_markup(msg, Markup.LEGACY)
+
+  def is_inlined(msg: XML.Tree): Boolean =
+    !(is_result(msg) || is_tracing(msg) || is_state(msg))
+
 
   /* dialogs */
 
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/System/isabelle_system.ML	Thu Apr 10 14:40:11 2014 +0200
@@ -67,7 +67,7 @@
   else (system_command ("cp -p -R -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
 
 
-(* unique tmp files *)
+(* tmp files *)
 
 fun create_tmp_path name ext =
   let
@@ -80,6 +80,9 @@
   let val path = create_tmp_path name ext
   in Exn.release (Exn.capture f path before ignore (try File.rm path)) end;
 
+
+(* tmp dirs *)
+
 fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path);
 
 fun with_tmp_dir name f =
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/build-jars	Thu Apr 10 14:40:11 2014 +0200
@@ -31,6 +31,7 @@
   General/symbol.scala
   General/time.scala
   General/timing.scala
+  General/url.scala
   General/xz_file.scala
   GUI/color_value.scala
   GUI/gui.scala
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Pure/goal_display.ML
--- a/src/Pure/goal_display.ML	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/goal_display.ML	Thu Apr 10 14:40:11 2014 +0200
@@ -15,7 +15,6 @@
   val show_consts: bool Config.T
   val pretty_flexpair: Proof.context -> term * term -> Pretty.T
   val pretty_goals: Proof.context -> thm -> Pretty.T list
-  val pretty_goals_without_context: thm -> Pretty.T list
   val pretty_goal: Proof.context -> thm -> Pretty.T
   val string_of_goal: Proof.context -> thm -> string
 end;
@@ -131,11 +130,6 @@
     (if show_sorts0 then pretty_varsT prop else [])
   end;
 
-fun pretty_goals_without_context th =
-  let val ctxt =
-    Config.put show_main_goal true (Syntax.init_pretty_global (Thm.theory_of_thm th))
-  in pretty_goals ctxt th end;
-
 val pretty_goal = Pretty.chunks oo pretty_goals;
 val string_of_goal = Pretty.string_of oo pretty_goal;
 
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/simplifier.ML	Thu Apr 10 14:40:11 2014 +0200
@@ -29,6 +29,19 @@
 sig
   include BASIC_SIMPLIFIER
   val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic
+  val attrib: (thm -> Proof.context -> Proof.context) -> attribute
+  val simp_add: attribute
+  val simp_del: attribute
+  val cong_add: attribute
+  val cong_del: attribute
+  val check_simproc: Proof.context -> xstring * Position.T -> string
+  val the_simproc: Proof.context -> string -> simproc
+  val def_simproc: {name: binding, lhss: term list,
+    proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} ->
+    local_theory -> local_theory
+  val def_simproc_cmd: {name: binding, lhss: string list,
+    proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} ->
+    local_theory -> local_theory
   val pretty_simpset: Proof.context -> Pretty.T
   val default_mk_sym: Proof.context -> thm -> thm option
   val prems_of: Proof.context -> thm list
@@ -57,19 +70,6 @@
   val full_rewrite: Proof.context -> conv
   val asm_lr_rewrite: Proof.context -> conv
   val asm_full_rewrite: Proof.context -> conv
-  val attrib: (thm -> Proof.context -> Proof.context) -> attribute
-  val simp_add: attribute
-  val simp_del: attribute
-  val cong_add: attribute
-  val cong_del: attribute
-  val check_simproc: Proof.context -> xstring * Position.T -> string
-  val the_simproc: Proof.context -> string -> simproc
-  val def_simproc: {name: binding, lhss: term list,
-    proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} ->
-    local_theory -> local_theory
-  val def_simproc_cmd: {name: binding, lhss: string list,
-    proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} ->
-    local_theory -> local_theory
   val cong_modifiers: Method.modifier parser list
   val simp_modifiers': Method.modifier parser list
   val simp_modifiers: Method.modifier parser list
@@ -83,36 +83,6 @@
 open Raw_Simplifier;
 
 
-(** pretty printing **)
-
-fun pretty_simpset ctxt =
-  let
-    val pretty_term = Syntax.pretty_term ctxt;
-    val pretty_thm = Display.pretty_thm ctxt;
-    val pretty_thm_item = Display.pretty_thm_item ctxt;
-
-    fun pretty_proc (name, lhss) =
-      Pretty.big_list (name ^ ":") (map (Pretty.item o single o pretty_term o Thm.term_of) lhss);
-
-    fun pretty_cong_name (const, name) =
-      pretty_term ((if const then Const else Free) (name, dummyT));
-    fun pretty_cong (name, thm) =
-      Pretty.block [pretty_cong_name name, Pretty.str ":", Pretty.brk 1, pretty_thm thm];
-
-    val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} =
-      dest_ss (simpset_of ctxt);
-  in
-    [Pretty.big_list "simplification rules:" (map (pretty_thm_item o #2) simps),
-      Pretty.big_list "simplification procedures:" (map pretty_proc (sort_wrt #1 procs)),
-      Pretty.big_list "congruences:" (map pretty_cong congs),
-      Pretty.strs ("loopers:" :: map quote loopers),
-      Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers),
-      Pretty.strs ("safe solvers:" :: map quote safe_solvers)]
-    |> Pretty.chunks
-  end;
-
-
-
 (** declarations **)
 
 (* attributes *)
@@ -187,6 +157,40 @@
 
 
 
+(** pretty_simpset **)
+
+fun pretty_simpset ctxt =
+  let
+    val pretty_term = Syntax.pretty_term ctxt;
+    val pretty_thm = Display.pretty_thm ctxt;
+    val pretty_thm_item = Display.pretty_thm_item ctxt;
+
+    fun pretty_simproc (name, lhss) =
+      Pretty.block
+        (Pretty.mark_str name :: Pretty.str ":" :: Pretty.fbrk ::
+          Pretty.fbreaks (map (Pretty.item o single o pretty_term o Thm.term_of) lhss));
+
+    fun pretty_cong_name (const, name) =
+      pretty_term ((if const then Const else Free) (name, dummyT));
+    fun pretty_cong (name, thm) =
+      Pretty.block [pretty_cong_name name, Pretty.str ":", Pretty.brk 1, pretty_thm thm];
+
+    val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} =
+      dest_ss (simpset_of ctxt);
+    val simprocs =
+      Name_Space.markup_entries ctxt (Name_Space.space_of_table (get_simprocs ctxt)) procs;
+  in
+    [Pretty.big_list "simplification rules:" (map (pretty_thm_item o #2) simps),
+      Pretty.big_list "simplification procedures:" (map pretty_simproc simprocs),
+      Pretty.big_list "congruences:" (map pretty_cong congs),
+      Pretty.strs ("loopers:" :: map quote loopers),
+      Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers),
+      Pretty.strs ("safe solvers:" :: map quote safe_solvers)]
+    |> Pretty.chunks
+  end;
+
+
+
 (** simplification tactics and rules **)
 
 fun solve_all_tac solvers ctxt =
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Pure/tactical.ML
--- a/src/Pure/tactical.ML	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/tactical.ML	Thu Apr 10 14:40:11 2014 +0200
@@ -30,7 +30,7 @@
   val FIRST': ('a -> tactic) list -> 'a -> tactic
   val FIRST1: (int -> tactic) list -> tactic
   val RANGE: (int -> tactic) list -> int -> tactic
-  val print_tac: string -> tactic
+  val print_tac: Proof.context -> string -> tactic
   val pause_tac: tactic
   val trace_REPEAT: bool Unsynchronized.ref
   val suppress_tracing: bool Unsynchronized.ref
@@ -182,9 +182,8 @@
 (*** Tracing tactics ***)
 
 (*Print the current proof state and pass it on.*)
-fun print_tac msg st =
- (tracing (msg ^ "\n" ^
-    Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals_without_context st)));
+fun print_tac ctxt msg st =
+ (tracing (msg ^ "\n" ^ Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals ctxt st)));
   Seq.single st);
 
 (*Pause until a line is typed -- if non-empty then fail. *)
@@ -223,7 +222,7 @@
 fun tracify flag tac st =
   if !flag andalso not (!suppress_tracing) then
     (tracing (Pretty.string_of (Pretty.chunks
-        (Goal_Display.pretty_goals_without_context st @
+        (Goal_Display.pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm st)) st @
           [Pretty.str "** Press RETURN to continue:"])));
      exec_trace_command flag (tac, st))
   else tac st;
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Sequents/prover.ML
--- a/src/Sequents/prover.ML	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Sequents/prover.ML	Thu Apr 10 14:40:11 2014 +0200
@@ -196,7 +196,7 @@
     val lastrestac = RESOLVE_THEN unsafes;
     fun gtac i =
       restac gtac i ORELSE
-       (if Config.get ctxt trace then print_tac "" THEN lastrestac gtac i
+       (if Config.get ctxt trace then print_tac ctxt "" THEN lastrestac gtac i
         else lastrestac gtac i)
   in gtac end;
 
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Tools/induction.ML
--- a/src/Tools/induction.ML	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Tools/induction.ML	Thu Apr 10 14:40:11 2014 +0200
@@ -17,7 +17,7 @@
   | (p as Free _, _) => [p]
   | (_, ts) => flat(map preds_of ts))
 
-fun name_hyps thy (arg as ((cases,consumes),th)) =
+fun name_hyps (arg as ((cases, consumes), th)) =
   if not(forall (null o #2 o #1) cases) then arg
   else
     let
@@ -35,7 +35,7 @@
         (take n cases ~~ take n hnamess)
     in ((cases',consumes),th) end
 
-val induction_tac = Induct.gen_induct_tac name_hyps
+val induction_tac = Induct.gen_induct_tac (K name_hyps)
 
 val setup = Induct.gen_induct_setup @{binding induction} induction_tac
 
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props	Thu Apr 10 14:40:11 2014 +0200
@@ -4,7 +4,7 @@
 
 #identification
 plugin.isabelle.jedit.Plugin.name=Isabelle
-plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Fabian Immler, Markus Kaiser, Makarius Wenzel
+plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Fabian Immler, Lars Hupel, Markus Kaiser, Makarius Wenzel
 plugin.isabelle.jedit.Plugin.version=1.0.0
 plugin.isabelle.jedit.Plugin.description=Isabelle Prover IDE
 
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Apr 10 14:40:11 2014 +0200
@@ -144,7 +144,7 @@
                 val line_range = Text.Range(start(i), end(i))
 
                 // gutter icons
-                rendering.gutter_message(line_range) match {
+                rendering.gutter_icon(line_range) match {
                   case Some(icon) =>
                     val x0 = (FOLD_MARKER_SIZE + width - border_width - icon.getIconWidth) max 10
                     val y0 = y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Thu Apr 10 14:40:11 2014 +0200
@@ -161,6 +161,7 @@
 
   def hyperlink_url(name: String): Hyperlink =
     new Hyperlink {
+      val external = true
       def follow(view: View) =
         default_thread_pool.submit(() =>
           try { Isabelle_System.open(name) }
@@ -173,6 +174,7 @@
 
   def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
     new Hyperlink {
+      val external = false
       def follow(view: View) = goto_file(view, name, line, column)
       override def toString: String = "file " + quote(name)
     }
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Apr 10 14:40:11 2014 +0200
@@ -10,10 +10,10 @@
 
 import isabelle._
 
-import java.io.{File => JFile, IOException, ByteArrayOutputStream}
+import java.io.{File => JFile, ByteArrayOutputStream}
 import javax.swing.text.Segment
 
-import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
+import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
 import org.gjt.sp.jedit.MiscUtilities
 import org.gjt.sp.jedit.{jEdit, View, Buffer}
 import org.gjt.sp.jedit.bufferio.BufferIORequest
@@ -45,6 +45,7 @@
   {
     val path = source_path.expand
     if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path)
+    else if (path.is_current) dir
     else {
       val vfs = VFSManager.getVFSForPath(dir)
       if (vfs.isInstanceOf[FileVFS])
@@ -54,42 +55,32 @@
     }
   }
 
-  override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
+  override def with_thy_text[A](name: Document.Node.Name, consume: CharSequence => A): A =
   {
     Swing_Thread.now {
       JEdit_Lib.jedit_buffer(name) match {
         case Some(buffer) =>
           JEdit_Lib.buffer_lock(buffer) {
-            Some(f(buffer.getSegment(0, buffer.getLength)))
+            Some(consume(buffer.getSegment(0, buffer.getLength)))
           }
         case None => None
       }
     } getOrElse {
-      val file = new JFile(name.node)  // FIXME load URL via jEdit VFS (!?)
-      if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
-      f(File.read(file))
+      if (Url.is_wellformed(name.node)) consume(Url.read(name.node))
+      else {
+        val file = new JFile(name.node)
+        if (file.isFile) consume(File.read(file))
+        else error("No such file: " + quote(file.toString))
+      }
     }
   }
 
-  def check_file(view: View, path: String): Boolean =
-  {
-    val vfs = VFSManager.getVFSForPath(path)
-    val session = vfs.createVFSSession(path, view)
-
+  def check_file(view: View, file: String): Boolean =
     try {
-      session != null && {
-        try {
-          val file = vfs._getFile(session, path, view)
-          file != null && file.isReadable && file.getType == VFSFile.FILE
-        }
-        catch { case _: IOException => false }
-      }
+      if (Url.is_wellformed(file)) Url.is_readable(file)
+      else (new JFile(file)).isFile
     }
-    finally {
-      try { vfs._endVFSSession(session, view) }
-      catch { case _: IOException => }
-    }
-  }
+    catch { case ERROR(_) => false }
 
 
   /* file content */
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Thu Apr 10 14:40:11 2014 +0200
@@ -36,6 +36,9 @@
     else None
   }
 
+  private def descendant(parent: JComponent): Option[Pretty_Tooltip] =
+    Swing_Thread.require { stack.find(tip => tip.original_parent == parent) }
+
   def apply(
     view: View,
     parent: JComponent,
@@ -60,7 +63,7 @@
             old.foreach(_.hide_popup)
 
             val loc = SwingUtilities.convertPoint(parent, location, layered)
-            val tip = new Pretty_Tooltip(view, layered, loc, rendering, results, info)
+            val tip = new Pretty_Tooltip(view, layered, parent, loc, rendering, results, info)
             stack = tip :: rest
             tip.show_popup
         }
@@ -142,6 +145,9 @@
     }
   }
 
+  def dismiss_descendant(parent: JComponent): Unit =
+    descendant(parent).foreach(dismiss(_))
+
   def dismissed_all(): Boolean =
   {
     deactivate()
@@ -159,6 +165,7 @@
 class Pretty_Tooltip private(
   view: View,
   layered: JLayeredPane,
+  val original_parent: JComponent,
   location: Point,
   rendering: Rendering,
   private val results: Command.Results,
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Thu Apr 10 14:40:11 2014 +0200
@@ -495,7 +495,14 @@
   lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
 
 
-  /* gutter icons */
+  /* gutter */
+
+  private def gutter_message_pri(msg: XML.Tree): Int =
+    if (Protocol.is_error(msg)) Rendering.error_pri
+    else if (Protocol.is_legacy(msg)) Rendering.legacy_pri
+    else if (Protocol.is_warning(msg)) Rendering.warning_pri
+    else if (Protocol.is_information(msg)) Rendering.information_pri
+    else 0
 
   private lazy val gutter_icons = Map(
     Rendering.information_pri -> JEdit_Lib.load_icon(options.string("gutter_information_icon")),
@@ -503,27 +510,17 @@
     Rendering.legacy_pri -> JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
     Rendering.error_pri -> JEdit_Lib.load_icon(options.string("gutter_error_icon")))
 
-  def gutter_message(range: Text.Range): Option[Icon] =
+  def gutter_icon(range: Text.Range): Option[Icon] =
   {
-    val results =
+    val pris =
       snapshot.cumulate[Int](range, 0, Rendering.gutter_elements, _ =>
         {
-          case (pri, Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _),
-              List(XML.Elem(Markup(Markup.INFORMATION, _), _))))) =>
-            Some(pri max Rendering.information_pri)
-          case (pri, Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body))) =>
-            body match {
-              case List(XML.Elem(Markup(Markup.LEGACY, _), _)) =>
-                Some(pri max Rendering.legacy_pri)
-              case _ =>
-                Some(pri max Rendering.warning_pri)
-            }
-          case (pri, Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _))) =>
-            Some(pri max Rendering.error_pri)
+          case (pri, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(serial)), _))) =>
+            Some(pri max gutter_message_pri(msg))
           case _ => None
-        })
-    val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
-    gutter_icons.get(pri)
+        }).map(_.info)
+
+    gutter_icons.get((0 /: pris)(_ max _))
   }
 
 
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Apr 10 14:40:11 2014 +0200
@@ -168,12 +168,14 @@
       robust_body(()) {
         hyperlink_area.info match {
           case Some(Text.Info(range, link)) =>
-            try { text_area.moveCaretPosition(range.start) }
-            catch {
-              case _: ArrayIndexOutOfBoundsException =>
-              case _: IllegalArgumentException =>
+            if (!link.external) {
+              try { text_area.moveCaretPosition(range.start) }
+              catch {
+                case _: ArrayIndexOutOfBoundsException =>
+                case _: IllegalArgumentException =>
+              }
+              text_area.requestFocus
             }
-            text_area.requestFocus
             link.follow(view)
           case None =>
         }
@@ -200,7 +202,8 @@
   private val mouse_motion_listener = new MouseMotionAdapter {
     override def mouseDragged(evt: MouseEvent) {
       robust_body(()) {
-        PIDE.dismissed_popups(view)
+        Completion_Popup.Text_Area.dismissed(text_area)
+        Pretty_Tooltip.dismiss_descendant(text_area.getPainter)
       }
     }
 
@@ -245,7 +248,7 @@
                         case Some(tip) =>
                           val painter = text_area.getPainter
                           val loc = new Point(x, y + painter.getFontMetrics.getHeight / 2)
-                          val results = rendering.command_results(range)
+                          val results = rendering.command_results(tip.range)
                           Pretty_Tooltip(view, painter, loc, rendering, results, tip)
                       }
                   }
diff -r 535cfc7fc301 -r b62c4e6d1b55 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Thu Apr 10 11:34:55 2014 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Thu Apr 10 14:40:11 2014 +0200
@@ -226,13 +226,13 @@
      rewrite_goals_tac ctxt con_defs,
      REPEAT (rtac @{thm refl} 2),
      (*Typechecking; this can fail*)
-     if !Ind_Syntax.trace then print_tac "The type-checking subgoal:"
+     if !Ind_Syntax.trace then print_tac ctxt "The type-checking subgoal:"
      else all_tac,
      REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
                         ORELSE' eresolve_tac (asm_rl :: @{thm PartE} :: @{thm SigmaE2} ::
                                               type_elims)
                         ORELSE' hyp_subst_tac ctxt1)),
-     if !Ind_Syntax.trace then print_tac "The subgoal after monos, type_elims:"
+     if !Ind_Syntax.trace then print_tac ctxt "The subgoal after monos, type_elims:"
      else all_tac,
      DEPTH_SOLVE (swap_res_tac (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];