diff --git a/src/HOL/Library/conditional_parametricity.ML b/src/HOL/Library/conditional_parametricity.ML
--- a/src/HOL/Library/conditional_parametricity.ML
+++ b/src/HOL/Library/conditional_parametricity.ML
@@ -1,519 +1,519 @@
 (*  Title:    HOL/Library/conditional_parametricity.ML
     Author:   Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel, ETH Zürich
 
 A conditional parametricity prover
 *)
 
 signature CONDITIONAL_PARAMETRICITY =
 sig
   exception WARNING of string
   type settings =
     {suppress_print_theorem: bool,
     suppress_warnings: bool,
     warnings_as_errors: bool,
     use_equality_heuristic: bool}
   val default_settings: settings
   val quiet_settings: settings
 
   val parametric_constant: settings -> Attrib.binding * thm -> Proof.context ->
     (thm * Proof.context)
   val get_parametricity_theorems: Proof.context -> thm list
 
   val prove_goal: settings -> Proof.context -> thm option -> term -> thm
   val prove_find_goal_cond: settings -> Proof.context -> thm list -> thm option -> term -> thm
 
   val mk_goal: Proof.context -> term -> term
   val mk_cond_goal: Proof.context -> thm -> term * thm
   val mk_param_goal_from_eq_def: Proof.context -> thm -> term
   val step_tac: settings -> Proof.context -> thm list -> int -> tactic
 end
 
 structure Conditional_Parametricity: CONDITIONAL_PARAMETRICITY =
 struct
 
 type settings =
   {suppress_print_theorem: bool,
   suppress_warnings: bool,
   warnings_as_errors: bool (* overrides suppress_warnings!  *),
   use_equality_heuristic: bool};
 
 val quiet_settings =
   {suppress_print_theorem = true,
   suppress_warnings = true,
   warnings_as_errors = false,
   use_equality_heuristic = false};
 
 val default_settings =
   {suppress_print_theorem = false,
   suppress_warnings = false,
   warnings_as_errors = false,
   use_equality_heuristic = false};
 
 (* helper functions *)
 
 fun strip_imp_prems_concl (Const("Pure.imp", _) $ A $ B) = A :: strip_imp_prems_concl B
   | strip_imp_prems_concl C = [C];
 
 fun strip_prop_safe t = Logic.unprotect t handle TERM _ => t;
 
 fun get_class_of ctxt t =
   Axclass.class_of_param (Proof_Context.theory_of ctxt) (fst (dest_Const t));
 
 fun is_class_op ctxt t =
   let
     val t' = t |> Envir.eta_contract;
   in
     Term.is_Const t' andalso is_some (get_class_of ctxt t')
   end;
 
 fun apply_Var_to_bounds t =
   let
     val (t, ts) = strip_comb t;
   in
     (case t of
       Var (xi, _) =>
         let
           val (bounds, tail) = chop_prefix is_Bound ts;
         in
           list_comb (Var (xi, fastype_of (betapplys (t, bounds))), map apply_Var_to_bounds tail)
         end
     | _ => list_comb (t, map apply_Var_to_bounds ts))
   end;
 
 fun theorem_format_error ctxt thm =
   let
     val msg = Pretty.string_of (Pretty.chunks [(Pretty.para
       "Unexpected format of definition. Must be an unconditional equation."), Thm.pretty_thm ctxt thm]);
   in error msg end;
 
 (* Tacticals and Tactics *)
 
 exception FINISH of thm;
 
 (* Tacticals *)
 fun REPEAT_TRY_ELSE_DEFER tac st =
   let
     fun COMB' tac count st = (
       let
         val n = Thm.nprems_of st;
       in
         (if n = 0 then all_tac st else
           (case Seq.pull ((tac THEN COMB' tac 0) st) of
             NONE =>
               if count+1 = n
               then raise FINISH st
               else (defer_tac 1 THEN (COMB' tac (count+1))) st
           | some => Seq.make (fn () => some)))
       end)
   in COMB' tac 0 st end;
 
 (* Tactics  *)
 (* helper tactics for printing *)
 fun error_tac ctxt msg st =
   (error (msg ^ "\n" ^ Goal_Display.string_of_goal ctxt st); Seq.single st);
 
 fun error_tac' ctxt msg = SELECT_GOAL (error_tac ctxt msg);
 
 (*  finds assumption of the form "Rel ?B Bound x Bound y", rotates it in front,
     applies rel_app arity times and uses ams_rl *)
 fun rel_app_tac ctxt t x y arity =
   let
     val rel_app = [@{thm Rel_app}];
     val assume = [asm_rl];
     fun find_and_rotate_tac t i =
       let
         fun is_correct_rule t =
           (case t of
             Const (\<^const_name>\<open>HOL.Trueprop\<close>, _) $ (Const (\<^const_name>\<open>Transfer.Rel\<close>, _) $
               _ $ Bound x' $ Bound y') => x = x' andalso y = y'
           | _ => false);
         val idx = find_index is_correct_rule (t |> Logic.strip_assums_hyp);
       in
         if idx < 0 then no_tac else rotate_tac idx i
       end;
     fun rotate_and_dresolve_tac ctxt arity i = REPEAT_DETERM_N (arity - 1)
       (EVERY' [rotate_tac ~1, dresolve_tac ctxt rel_app, defer_tac] i);
   in
     SELECT_GOAL (EVERY' [find_and_rotate_tac t, forward_tac ctxt rel_app, defer_tac,
       rotate_and_dresolve_tac ctxt arity, rotate_tac ~1, eresolve_tac ctxt assume] 1)
   end;
 
 exception WARNING of string;
 
 fun transform_rules 0 thms = thms
   | transform_rules n thms = transform_rules (n - 1) (curry (Drule.RL o swap)
       @{thms Rel_app Rel_match_app} thms);
 
 fun assume_equality_tac settings ctxt t arity i st =
   let
     val quiet = #suppress_warnings settings;
     val errors = #warnings_as_errors settings;
     val T = fastype_of t;
     val is_eq_lemma = @{thm is_equality_Rel} |> Thm.incr_indexes ((Term.maxidx_of_term t) + 1) |>
       Drule.infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt t)];
     val msg = Pretty.string_of (Pretty.chunks [Pretty.paragraph ((Pretty.text
       "No rule found for constant \"") @ [Syntax.pretty_term ctxt t, Pretty.str " :: " ,
       Syntax.pretty_typ ctxt T] @ (Pretty.text "\". Using is_eq_lemma:")), Pretty.quote
       (Thm.pretty_thm ctxt is_eq_lemma)]);
     fun msg_tac st = (if errors then raise WARNING msg else if quiet then () else warning msg;
       Seq.single st)
     val tac = resolve_tac ctxt (transform_rules arity [is_eq_lemma]) i;
   in
     (if fold_atyps (K (K true)) T false then msg_tac THEN tac else tac) st
   end;
 
 fun mark_class_as_match_tac ctxt const const' arity =
   let
     val rules = transform_rules arity [@{thm Rel_match_Rel} |> Thm.incr_indexes ((Int.max o
       apply2 Term.maxidx_of_term) (const, const') + 1) |> Drule.infer_instantiate' ctxt [NONE,
       SOME (Thm.cterm_of ctxt const), SOME (Thm.cterm_of ctxt const')]];
   in resolve_tac ctxt rules end;
 
 (* transforms the parametricity theorems to fit a given arity and uses them for resolution *)
 fun parametricity_thm_tac settings ctxt parametricity_thms const arity =
   let
     val rules = transform_rules arity parametricity_thms;
   in resolve_tac ctxt rules ORELSE' assume_equality_tac settings ctxt const arity end;
 
 (* variant of parametricity_thm_tac to use matching *)
 fun parametricity_thm_match_tac ctxt parametricity_thms arity =
    let
     val rules = transform_rules arity parametricity_thms;
   in match_tac ctxt rules end;
 
 fun rel_abs_tac ctxt = resolve_tac ctxt [@{thm Rel_abs}];
 
 fun step_tac' settings ctxt parametricity_thms (tm, i) =
   (case tm |> Logic.strip_assums_concl of
     Const (\<^const_name>\<open>HOL.Trueprop\<close>, _) $ (Const (rel, _) $ _ $ t $ u) =>
     let
       val (arity_of_t, arity_of_u) = apply2 (strip_comb #> snd #> length) (t, u);
     in
       (case rel of
         \<^const_name>\<open>Transfer.Rel\<close> =>
           (case (head_of t, head_of u) of
             (Abs _, _) => rel_abs_tac ctxt
           | (_, Abs _) => rel_abs_tac ctxt
           | (const as (Const _), const' as (Const _)) =>
             if #use_equality_heuristic settings andalso t aconv u
               then
                 assume_equality_tac quiet_settings ctxt t 0
               else if arity_of_t = arity_of_u
                 then if is_class_op ctxt const orelse is_class_op ctxt const'
                   then mark_class_as_match_tac ctxt const const' arity_of_t
                   else parametricity_thm_tac settings ctxt parametricity_thms const arity_of_t
                 else error_tac' ctxt "Malformed term. Arities of t and u don't match."
           | (Bound x, Bound y) =>
             if arity_of_t = arity_of_u then if arity_of_t > 0 then rel_app_tac ctxt tm x y arity_of_t
                else assume_tac ctxt
             else  error_tac' ctxt "Malformed term. Arities of t and u don't match."
           | _ => error_tac' ctxt
             "Unexpected format. Expected  (Abs _, _), (_, Abs _), (Const _, Const _) or (Bound _, Bound _).")
          | \<^const_name>\<open>Conditional_Parametricity.Rel_match\<close> =>
              parametricity_thm_match_tac ctxt parametricity_thms arity_of_t
       | _ => error_tac' ctxt "Unexpected format. Expected Transfer.Rel or Rel_match marker." ) i
     end
     | Const (\<^const_name>\<open>HOL.Trueprop\<close>, _) $ (Const (\<^const_name>\<open>Transfer.is_equality\<close>, _) $ _) =>
         Transfer.eq_tac ctxt i
     | _ => error_tac' ctxt "Unexpected format. Not of form Const (HOL.Trueprop, _) $ _" i);
 
 fun step_tac settings = SUBGOAL oo step_tac' settings;
 
 fun apply_theorem_tac ctxt thm =
   HEADGOAL (resolve_tac ctxt [Local_Defs.unfold ctxt @{thms Pure.prop_def} thm] THEN_ALL_NEW
     assume_tac ctxt);
 
 (* Goal Generation  *)
 fun strip_boundvars_from_rel_match t =
   (case t of
     (Tp as Const (\<^const_name>\<open>HOL.Trueprop\<close>, _)) $
       ((Rm as Const (\<^const_name>\<open>Conditional_Parametricity.Rel_match\<close>, _)) $ R $ t $ t') =>
         Tp $ (Rm $ apply_Var_to_bounds R $ t $ t')
   | _ => t);
 
 val extract_conditions =
   let
     val filter_bounds = filter_out Term.is_open;
     val prem_to_conditions =
       map (map strip_boundvars_from_rel_match o strip_imp_prems_concl o strip_all_body);
     val remove_duplicates = distinct Term.aconv;
   in remove_duplicates o filter_bounds o flat o prem_to_conditions end;
 
 fun mk_goal ctxt t =
   let
     val ctxt = fold (Variable.declare_typ o snd) (Term.add_frees t []) ctxt;
     val t = singleton (Variable.polymorphic ctxt) t;
     val i = maxidx_of_term t + 1;
     fun tvar_to_tfree ((name, _), sort) = (name, sort);
     val tvars = Term.add_tvars t [];
     val new_frees = map TFree (Term.variant_frees t (map tvar_to_tfree tvars));
     val u = subst_atomic_types ((map TVar tvars) ~~ new_frees) t;
     val T = fastype_of t;
     val U = fastype_of u;
     val R = [T,U] ---> \<^typ>\<open>bool\<close>
     val r = Var (("R", 2 * i), R);
     val transfer_rel = Const (\<^const_name>\<open>Transfer.Rel\<close>, [R,T,U] ---> \<^typ>\<open>bool\<close>);
   in HOLogic.mk_Trueprop (transfer_rel $ r $ t $ u) end;
 
 fun mk_abs_helper T t =
   let
     val U = fastype_of t;
     fun mk_abs_helper' T U =
       if T = U then t else
         let
           val (T2, T1) = Term.dest_funT T;
         in
           Term.absdummy T2 (mk_abs_helper' T1 U)
         end;
   in mk_abs_helper' T U end;
 
 fun compare_ixs ((name, i):indexname, (name', i'):indexname) = if name < name' then LESS
   else if name > name' then GREATER
   else if i < i' then LESS
   else if i > i' then GREATER
   else EQUAL;
 
 fun mk_cond_goal ctxt thm =
   let
     val conclusion = (hd o strip_imp_prems_concl o strip_prop_safe o Thm.concl_of) thm;
     val conditions = (extract_conditions o Thm.prems_of) thm;
     val goal = Logic.list_implies (conditions, conclusion);
     fun compare ((ix, _), (ix', _)) = compare_ixs (ix, ix');
     val goal_vars = Term.add_vars goal [] |> Ord_List.make compare;
     val (ixs, Ts) = split_list goal_vars;
     val (_, Ts') = Term.add_vars (Thm.prop_of thm) [] |> Ord_List.make compare
       |> Ord_List.inter compare goal_vars |> split_list;
     val (As, _) = Ctr_Sugar_Util.mk_Frees "A" Ts ctxt;
     val goal_subst = ixs ~~ As;
     val thm_subst = ixs ~~ (map2 mk_abs_helper Ts' As);
     val thm' = thm |> Drule.infer_instantiate ctxt (map (apsnd (Thm.cterm_of ctxt)) thm_subst);
   in (goal |> Term.subst_Vars goal_subst, thm') end;
 
 fun mk_param_goal_from_eq_def ctxt thm =
   let
     val t =
       (case Thm.full_prop_of thm of
         (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t' $ _) => t'
       | _ => theorem_format_error ctxt thm);
   in mk_goal ctxt t end;
 
 (* Transformations and parametricity theorems *)
 fun transform_class_rule ctxt thm =
   (case Thm.concl_of thm of
     Const (\<^const_name>\<open>HOL.Trueprop\<close>, _) $ (Const (\<^const_name>\<open>Transfer.Rel\<close>, _) $ _ $ t $ u ) =>
       (if curry Term.aconv_untyped t u andalso is_class_op ctxt t then
         thm RS @{thm Rel_Rel_match}
       else thm)
   | _ => thm);
 
 fun is_parametricity_theorem thm =
   (case Thm.concl_of thm of
     Const (\<^const_name>\<open>HOL.Trueprop\<close>, _) $ (Const (rel, _) $ _ $ t $ u ) =>
       if rel = \<^const_name>\<open>Transfer.Rel\<close> orelse
         rel = \<^const_name>\<open>Conditional_Parametricity.Rel_match\<close>
       then curry Term.aconv_untyped t u
       else false
   | _ => false);
 
 (* Pre- and postprocessing of theorems *)
 fun mk_Domainp_assm (T, R) =
   HOLogic.mk_eq ((Const (\<^const_name>\<open>Domainp\<close>, Term.fastype_of T --> Term.fastype_of R) $ T), R);
 
 val Domainp_lemma =
   @{lemma "(!!R. Domainp T = R ==> PROP (P R)) == PROP (P (Domainp T))"
     by (rule, drule meta_spec,
       erule meta_mp, rule HOL.refl, simp)};
 
 fun fold_Domainp f (t as Const (\<^const_name>\<open>Domainp\<close>,_) $ (Var (_,_))) = f t
   | fold_Domainp f (t $ u) = fold_Domainp f t #> fold_Domainp f u
   | fold_Domainp f (Abs (_, _, t)) = fold_Domainp f t
   | fold_Domainp _ _ = I;
 
 fun subst_terms tab t =
   let
     val t' = Termtab.lookup tab t
   in
     (case t' of
       SOME t' => t'
     | NONE =>
       (case t of
           u $ v => (subst_terms tab u) $ (subst_terms tab v)
         | Abs (a, T, t) => Abs (a, T, subst_terms tab t)
         | t => t))
   end;
 
 fun gen_abstract_domains ctxt (dest : term -> term * (term -> term)) thm =
   let
     val prop = Thm.prop_of thm
     val (t, mk_prop') = dest prop
     val Domainp_ts = rev (fold_Domainp (fn t => insert op= t) t [])
     val Domainp_Ts = map (snd o dest_funT o snd o dest_Const o fst o dest_comb) Domainp_ts
     val used = Term.add_free_names t []
     val rels = map (snd o dest_comb) Domainp_ts
     val rel_names = map (fst o fst o dest_Var) rels
     val names = map (fn name => ("D" ^ name)) rel_names |> Name.variant_list used
     val frees = map Free (names ~~ Domainp_Ts)
     val prems = map (HOLogic.mk_Trueprop o mk_Domainp_assm) (rels ~~ frees);
     val t' = subst_terms (fold Termtab.update (Domainp_ts ~~ frees) Termtab.empty) t
     val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
     val prop2 = Logic.list_rename_params (rev names) prop1
     val cprop = Thm.cterm_of ctxt prop2
     val equal_thm = Raw_Simplifier.rewrite ctxt false [Domainp_lemma] cprop
     fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
   in
     forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
   end
     handle TERM _ => thm;
 
 fun abstract_domains_transfer ctxt thm =
   let
     fun dest prop =
       let
         val prems = Logic.strip_imp_prems prop
         val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
         val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
       in
         (x, fn x' =>
           Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x' $ y)))
       end
   in
     gen_abstract_domains ctxt dest thm
   end;
 
 fun transfer_rel_conv conv =
   Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.fun2_conv (Conv.arg_conv conv)));
 
 fun fold_relator_eqs_conv ctxt =
   Conv.bottom_rewrs_conv (Transfer.get_relator_eq ctxt) ctxt;
 
 fun mk_is_equality t =
   Const (\<^const_name>\<open>is_equality\<close>, Term.fastype_of t --> HOLogic.boolT) $ t;
 
 val is_equality_lemma =
   @{lemma "(!!R. is_equality R ==> PROP (P R)) == PROP (P (=))"
     by (unfold is_equality_def, rule, drule meta_spec,
       erule meta_mp, rule HOL.refl, simp)};
 
 fun gen_abstract_equalities ctxt (dest : term -> term * (term -> term)) thm =
   let
     val prop = Thm.prop_of thm
     val (t, mk_prop') = dest prop
     (* Only consider "(=)" at non-base types *)
     fun is_eq (Const (\<^const_name>\<open>HOL.eq\<close>, Type ("fun", [T, _]))) =
         (case T of Type (_, []) => false | _ => true)
       | is_eq _ = false
     val add_eqs = Term.fold_aterms (fn t => if is_eq t then insert (op =) t else I)
     val eq_consts = rev (add_eqs t [])
     val eqTs = map (snd o dest_Const) eq_consts
     val used = Term.add_free_names prop []
     val names = map (K "") eqTs |> Name.variant_list used
     val frees = map Free (names ~~ eqTs)
     val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees
     val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
     val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
     val cprop = Thm.cterm_of ctxt prop2
     val equal_thm = Raw_Simplifier.rewrite ctxt false [is_equality_lemma] cprop
     fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
   in
     forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
   end
     handle TERM _ => thm;
 
 fun abstract_equalities_transfer ctxt thm =
   let
     fun dest prop =
       let
         val prems = Logic.strip_imp_prems prop
         val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
         val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
       in
         (rel, fn rel' =>
           Logic.list_implies (prems, HOLogic.mk_Trueprop (rel' $ x $ y)))
       end
     val contracted_eq_thm =
       Conv.fconv_rule (transfer_rel_conv (fold_relator_eqs_conv ctxt)) thm
       handle CTERM _ => thm
   in
     gen_abstract_equalities ctxt dest contracted_eq_thm
   end;
 
 fun prep_rule ctxt = abstract_equalities_transfer ctxt #> abstract_domains_transfer ctxt;
 
 fun get_preprocess_theorems ctxt =
   Named_Theorems.get ctxt \<^named_theorems>\<open>parametricity_preprocess\<close>;
 
 fun preprocess_theorem ctxt =
   Local_Defs.unfold0 ctxt (get_preprocess_theorems ctxt)
   #> transform_class_rule ctxt;
 
 fun postprocess_theorem ctxt =
   Local_Defs.fold ctxt (@{thm Rel_Rel_match_eq} :: get_preprocess_theorems ctxt)
   #> prep_rule ctxt
   #>  Local_Defs.unfold ctxt @{thms Rel_def};
 
 fun get_parametricity_theorems ctxt =
   let
     val parametricity_thm_map_filter =
       Option.filter (is_parametricity_theorem andf (not o curry Term.could_unify
         (Thm.full_prop_of @{thm is_equality_Rel})) o Thm.full_prop_of) o preprocess_theorem ctxt;
   in
     map_filter (parametricity_thm_map_filter o Thm.transfer' ctxt)
       (Transfer.get_transfer_raw ctxt)
   end;
 
 (* Provers *)
 (* Tries to prove a parametricity theorem without conditions, returns the last goal_state as thm *)
 fun prove_find_goal_cond settings ctxt rules def_thm t =
   let
     fun find_conditions_tac {context = ctxt, prems = _} = unfold_tac ctxt (the_list def_thm) THEN
       (REPEAT_TRY_ELSE_DEFER o HEADGOAL) (step_tac settings ctxt rules);
   in
     Goal.prove ctxt [] [] t find_conditions_tac handle FINISH st => st
   end;
 
 (* Simplifies and proves thm *)
 fun prove_cond_goal ctxt thm =
   let
     val (goal, thm') = mk_cond_goal ctxt thm;
     val vars = Variable.add_free_names ctxt goal [];
     fun prove_conditions_tac {context = ctxt, prems = _} = apply_theorem_tac ctxt thm';
     val vars = Variable.add_free_names ctxt (Thm.prop_of thm') vars;
   in
     Goal.prove ctxt vars [] goal prove_conditions_tac
   end;
 
 (* Finds necessary conditions for t and proofs conditional parametricity of t under those conditions *)
 fun prove_goal settings ctxt def_thm t =
   let
     val parametricity_thms = get_parametricity_theorems ctxt;
     val found_thm = prove_find_goal_cond settings ctxt parametricity_thms def_thm t;
     val thm = prove_cond_goal ctxt found_thm;
   in
     postprocess_theorem ctxt thm
   end;
 
 (* Commands  *)
 fun gen_parametric_constant settings prep_att prep_thm (raw_b : Attrib.binding, raw_eq) lthy =
   let
     val b = apsnd (map (prep_att lthy)) raw_b;
     val def_thm = (prep_thm lthy raw_eq);
     val eq = Ctr_Sugar_Util.mk_abs_def def_thm handle TERM _ => theorem_format_error lthy def_thm;
     val goal= mk_param_goal_from_eq_def lthy eq;
     val thm = prove_goal settings lthy (SOME eq) goal;
     val (res, lthy') = Local_Theory.note (b, [thm]) lthy;
     val _ = if #suppress_print_theorem settings then () else
-      Proof_Display.print_results true (Position.thread_data ()) lthy' (("theorem",""), [res]);
+      Proof_Display.print_theorem (Position.thread_data ()) lthy' res;
   in
     (the_single (snd res), lthy')
   end;
 
 fun parametric_constant settings = gen_parametric_constant settings (K I) (K I);
 
 val parametric_constant_cmd = snd oo gen_parametric_constant default_settings (Attrib.check_src)
   (singleton o Attrib.eval_thms);
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>parametric_constant\<close> "proves parametricity"
     ((Parse_Spec.opt_thm_name ":" -- Parse.thm) >> parametric_constant_cmd);
 
 end;
diff --git a/src/Pure/Isar/proof_display.ML b/src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML
+++ b/src/Pure/Isar/proof_display.ML
@@ -1,422 +1,426 @@
 (*  Title:      Pure/Isar/proof_display.ML
     Author:     Makarius
 
 Printing of theorems, goals, results etc.
 *)
 
 signature PROOF_DISPLAY =
 sig
   val pp_context: Proof.context -> Pretty.T
   val pp_thm: (unit -> theory) -> thm -> Pretty.T
   val pp_typ: (unit -> theory) -> typ -> Pretty.T
   val pp_term: (unit -> theory) -> term -> Pretty.T
   val pp_ctyp: (unit -> theory) -> ctyp -> Pretty.T
   val pp_cterm: (unit -> theory) -> cterm -> Pretty.T
   val pretty_theory: bool -> Proof.context -> Pretty.T
   val pretty_definitions: bool -> Proof.context -> Pretty.T
   val pretty_theorems_diff: bool -> theory list -> Proof.context -> Pretty.T list
   val pretty_theorems: bool -> Proof.context -> Pretty.T list
   val string_of_rule: Proof.context -> string -> thm -> string
   val pretty_goal_header: thm -> Pretty.T
   val string_of_goal: Proof.context -> thm -> string
   val pretty_goal_facts: Proof.context -> string -> thm list option -> Pretty.T list
   val pretty_goal_inst: Proof.context -> term list list -> thm -> Pretty.T list
   val method_error: string -> Position.T ->
     {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
   val show_results: bool Config.T
   val print_results: bool -> Position.T -> Proof.context ->
     ((string * string) * (string * thm list) list) -> unit
+  val print_theorem: Position.T -> Proof.context -> string * thm list -> unit
   val print_consts: bool -> Position.T -> Proof.context ->
     (string * typ -> bool) -> (string * typ) list -> unit
   val markup_extern_label: Position.T -> (Markup.T * xstring) option
   val print_label: Position.T -> string
   val print_context_tracing: Context.generic * Position.T -> string
 end
 
 structure Proof_Display: PROOF_DISPLAY =
 struct
 
 (** toplevel pretty printing **)
 
 fun pp_context ctxt =
  (if Config.get ctxt Proof_Context.debug then
     Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
   else Pretty.str "<context>");
 
 fun default_context mk_thy =
   (case Context.get_generic_context () of
     SOME (Context.Proof ctxt) => ctxt
   | SOME (Context.Theory thy) =>
       try Syntax.init_pretty_global thy
       |> \<^if_none>\<open>Syntax.init_pretty_global (mk_thy ())\<close>
   | NONE => Syntax.init_pretty_global (mk_thy ()));
 
 fun pp_thm mk_thy th =
   Thm.pretty_thm_raw (default_context mk_thy) {quote = true, show_hyps = false} th;
 
 fun pp_typ mk_thy T = Pretty.quote (Syntax.pretty_typ (default_context mk_thy) T);
 fun pp_term mk_thy t = Pretty.quote (Syntax.pretty_term (default_context mk_thy) t);
 
 fun pp_ctyp mk_thy cT = pp_typ mk_thy (Thm.typ_of cT);
 fun pp_cterm mk_thy ct = pp_term mk_thy (Thm.term_of ct);
 
 
 
 (** theory content **)
 
 fun pretty_theory verbose ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
 
     fun prt_cls c = Syntax.pretty_sort ctxt [c];
     fun prt_sort S = Syntax.pretty_sort ctxt S;
     fun prt_arity t (c, Ss) = Syntax.pretty_arity ctxt (t, Ss, [c]);
     fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty);
     val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global;
     fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
     val prt_term_no_vars = prt_term o Logic.unvarify_global;
     fun prt_const (c, ty) = [Pretty.mark_str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
 
     fun pretty_classrel (c, []) = prt_cls c
       | pretty_classrel (c, cs) = Pretty.block
           (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: Pretty.commas (map prt_cls cs));
 
     fun pretty_default S = Pretty.block
       [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
 
     val tfrees = map (fn v => TFree (v, []));
     fun pretty_type syn (t, Type.LogicalType n) =
           if syn then NONE
           else SOME (prt_typ (Type (t, tfrees (Name.invent Name.context Name.aT n))))
       | pretty_type syn (t, Type.Abbreviation (vs, U, syn')) =
           if syn <> syn' then NONE
           else SOME (Pretty.block
             [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U])
       | pretty_type syn (t, Type.Nonterminal) =
           if not syn then NONE
           else SOME (prt_typ (Type (t, [])));
 
     val pretty_arities = maps (fn (t, ars) => map (prt_arity t) ars);
 
     fun pretty_abbrev (c, (ty, t)) = Pretty.block
       (prt_const (c, ty) @ [Pretty.str " \<equiv>", Pretty.brk 1, prt_term_no_vars t]);
 
     val tsig = Sign.tsig_of thy;
     val consts = Sign.consts_of thy;
     val {const_space, constants, constraints} = Consts.dest consts;
     val {classes, default, types, ...} = Type.rep_tsig tsig;
     val type_space = Type.type_space tsig;
     val (class_space, class_algebra) = classes;
     val classes = Sorts.classes_of class_algebra;
     val arities = Sorts.arities_of class_algebra;
 
     val clsses =
       Name_Space.extern_entries verbose ctxt class_space
         (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes))
       |> map (apfst #1);
     val tdecls = Name_Space.extern_table verbose ctxt types |> map (apfst #1);
     val arties =
       Name_Space.extern_entries verbose ctxt type_space (Symtab.dest arities)
       |> map (apfst #1);
 
     val cnsts = Name_Space.markup_entries verbose ctxt const_space constants;
     val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
     val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
     val cnstrs = Name_Space.markup_entries verbose ctxt const_space constraints;
   in
     Pretty.chunks
      [Pretty.big_list "classes:" (map pretty_classrel clsses),
       pretty_default default,
       Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls),
       Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls),
       Pretty.big_list "type arities:" (pretty_arities arties),
       Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts),
       Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
       Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
       Pretty.block
         (Pretty.breaks (Pretty.str "oracles:" ::
           map Pretty.mark_str (Thm.extern_oracles verbose ctxt)))]
   end;
 
 
 (* theorems *)
 
 fun pretty_theorems_diff verbose prev_thys ctxt =
   let
     val pretty_fact = Proof_Context.pretty_fact ctxt;
     val facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt);
     val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts;
     val prts = map #1 (sort_by (#1 o #2) (map (`pretty_fact) thmss));
   in if null prts then [] else [Pretty.big_list "theorems:" prts] end;
 
 fun pretty_theorems verbose ctxt =
   pretty_theorems_diff verbose (Theory.parents_of (Proof_Context.theory_of ctxt)) ctxt;
 
 
 (* definitions *)
 
 fun pretty_definitions verbose ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
     val context = Proof_Context.defs_context ctxt;
 
     val const_space = Proof_Context.const_space ctxt;
     val type_space = Proof_Context.type_space ctxt;
     val item_space = fn Defs.Const => const_space | Defs.Type => type_space;
     fun prune_item (k, c) = not verbose andalso Name_Space.is_concealed (item_space k) c;
 
     fun extern_item (kind, name) =
       let val xname = Name_Space.extern ctxt (item_space kind) name
       in (xname, (kind, name)) end;
 
     fun extern_item_ord ((xname1, (kind1, _)), (xname2, (kind2, _))) =
       (case Defs.item_kind_ord (kind1, kind2) of
         EQUAL => string_ord (xname1, xname2)
       | ord => ord);
 
     fun sort_items f = sort (extern_item_ord o apply2 f);
 
     fun pretty_entry ((_: string, item), args) = Defs.pretty_entry context (item, args);
 
     fun pretty_reduct (lhs, rhs) = Pretty.block
       ([pretty_entry lhs, Pretty.str "  ->", Pretty.brk 2] @
         Pretty.commas (map pretty_entry (sort_items fst rhs)));
 
     fun pretty_restrict (entry, name) =
       Pretty.block ([pretty_entry entry, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
 
     val defs = Theory.defs_of thy;
     val {restricts, reducts} = Defs.dest defs;
 
     val (reds1, reds2) =
       filter_out (prune_item o #1 o #1) reducts
       |> map (fn (lhs, rhs) =>
         (apfst extern_item lhs, map (apfst extern_item) (filter_out (prune_item o fst) rhs)))
       |> sort_items (#1 o #1)
       |> filter_out (null o #2)
       |> List.partition (Defs.plain_args o #2 o #1);
 
     val rests = restricts |> map (apfst (apfst extern_item)) |> sort_items (#1 o #1);
   in
     Pretty.big_list "definitions:"
       (map (Pretty.text_fold o single)
         [Pretty.big_list "non-overloaded LHS:" (map pretty_reduct reds1),
          Pretty.big_list "overloaded LHS:" (map pretty_reduct reds2),
          Pretty.big_list "pattern restrictions due to incomplete LHS:" (map pretty_restrict rests)])
   end;
 
 
 
 (** proof items **)
 
 (* refinement rule *)
 
 fun pretty_rule ctxt s thm =
   Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
     Pretty.fbrk, Thm.pretty_thm ctxt thm];
 
 val string_of_rule = Pretty.string_of ooo pretty_rule;
 
 
 (* goals *)
 
 local
 
 fun subgoals 0 = []
   | subgoals 1 = [Pretty.brk 1, Pretty.str "(1 subgoal)"]
   | subgoals n = [Pretty.brk 1, Pretty.str ("(" ^ string_of_int n ^ " subgoals)")];
 
 in
 
 fun pretty_goal_header goal =
   Pretty.block ([Pretty.keyword1 "goal"] @ subgoals (Thm.nprems_of goal) @ [Pretty.str ":"]);
 
 end;
 
 fun string_of_goal ctxt goal =
   Pretty.string_of (Pretty.chunks [pretty_goal_header goal, Goal_Display.pretty_goal ctxt goal]);
 
 
 (* goal facts *)
 
 fun pretty_goal_facts _ _ NONE = []
   | pretty_goal_facts ctxt s (SOME ths) =
       (single o Pretty.block o Pretty.fbreaks)
         [if s = "" then Pretty.str "this:"
          else Pretty.block [Pretty.keyword1 s, Pretty.brk 1, Pretty.str "this:"],
          Proof_Context.pretty_fact ctxt ("", ths)];
 
 
 (* goal instantiation *)
 
 fun pretty_goal_inst ctxt propss goal =
   let
     val title = "goal instantiation:";
 
     fun prt_inst env =
       if Envir.is_empty env then []
       else
         let
           val Envir.Envir {tyenv, tenv, ...} = env;
 
           val prt_type = Syntax.pretty_typ ctxt;
           val prt_term = Syntax.pretty_term ctxt;
 
           fun instT v =
             let
               val T = TVar v;
               val T' = Envir.subst_type tyenv T;
             in if T = T' then NONE else SOME (prt_type T, prt_type T') end;
 
           fun inst v =
             let
               val t = Var v;
               val t' = Envir.subst_term (tyenv, tenv) (Envir.subst_term_types tyenv t);
             in if t aconv t' then NONE else SOME (prt_term t, prt_term t') end;
 
           fun inst_pair (x, y) = Pretty.item [x, Pretty.str " \<leadsto>", Pretty.brk 1, y];
 
           val prts =
             ((fold o fold) Term.add_tvars propss [] |> sort Term_Ord.tvar_ord |> map_filter instT) @
             ((fold o fold) Term.add_vars propss [] |> sort Term_Ord.var_ord |> map_filter inst);
         in if null prts then [] else [Pretty.big_list title (map inst_pair prts)] end;
 
     exception LOST_STRUCTURE;
     fun goal_matcher () =
       let
         val concl =
           Logic.unprotect (Thm.concl_of goal)
             handle TERM _ => raise LOST_STRUCTURE;
         val goal_propss = filter_out null propss;
         val results =
           Logic.dest_conjunction_balanced (length goal_propss) concl
           |> map2 Logic.dest_conjunction_balanced (map length goal_propss)
             handle TERM _ => raise LOST_STRUCTURE;
       in
         Unify.matcher (Context.Proof ctxt)
           (map (Soft_Type_System.purge ctxt) (flat goal_propss)) (flat results)
       end;
 
     fun failure msg = (warning (title ^ " " ^ msg); []);
   in
     (case goal_matcher () of
       SOME env => prt_inst env
     | NONE => failure "match failed")
     handle LOST_STRUCTURE => failure "lost goal structure"
   end;
 
 
 (* method_error *)
 
 fun method_error kind pos {context = ctxt, facts, goal} = Seq.Error (fn () =>
   let
     val pr_header =
       "Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^
       "proof method" ^ Position.here pos ^ ":\n";
     val pr_facts =
       if null facts then ""
       else Pretty.string_of (Pretty.chunks (pretty_goal_facts ctxt "using" (SOME facts))) ^ "\n";
     val pr_goal = string_of_goal ctxt goal;
   in pr_header ^ pr_facts ^ pr_goal end);
 
 
 (* results *)
 
 fun position_markup pos = Pretty.mark (Position.markup pos Markup.position);
 
 val interactive =
   Config.declare_bool ("interactive", \<^here>) (K false);
 
 val show_results =
   Attrib.setup_config_bool \<^binding>\<open>show_results\<close>
     (fn context =>
       Config.get_generic context interactive orelse
       Options.default_bool \<^system_option>\<open>show_states\<close>);
 
 fun no_print int ctxt = not (Config.get (Config.put interactive int ctxt) show_results);
 
 local
 
 fun pretty_fact_name pos (kind, "") = position_markup pos (Pretty.keyword1 kind)
   | pretty_fact_name pos (kind, name) =
       Pretty.block [position_markup pos (Pretty.keyword1 kind), Pretty.brk 1,
         Pretty.str (Long_Name.base_name name), Pretty.str ":"];
 
 fun pretty_facts ctxt =
   flat o (separate [Pretty.fbrk, Pretty.keyword2 "and", Pretty.str " "]) o
     map (single o Proof_Context.pretty_fact ctxt);
 
 in
 
 fun print_results int pos ctxt ((kind, name), facts) =
   if kind = "" orelse no_print int ctxt then ()
   else if name = "" then
     (Output.state o Pretty.string_of)
       (Pretty.block (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
         pretty_facts ctxt facts))
   else
     (Output.state o Pretty.string_of)
       (case facts of
         [fact] => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
           Proof_Context.pretty_fact ctxt fact])
       | _ => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
           Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
 
+fun print_theorem pos ctxt fact =
+  print_results true pos ctxt ((Thm.theoremK, ""), [fact]);
+
 end;
 
 
 (* consts *)
 
 local
 
 fun pretty_var ctxt (x, T) =
   Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
     Pretty.quote (Syntax.pretty_typ ctxt T)];
 
 fun pretty_vars pos ctxt kind vs =
   Pretty.block
     (Pretty.fbreaks (position_markup pos (Pretty.mark_str kind) :: map (pretty_var ctxt) vs));
 
 val fixes = (Markup.keyword2, "fixes");
 val consts = (Markup.keyword1, "consts");
 
 fun pretty_consts pos ctxt pred cs =
   (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of
     [] => pretty_vars pos ctxt consts cs
   | ps => Pretty.chunks [pretty_vars pos ctxt fixes ps, pretty_vars pos ctxt consts cs]);
 
 in
 
 fun print_consts int pos ctxt pred cs =
   if null cs orelse no_print int ctxt then ()
   else Output.state (Pretty.string_of (pretty_consts pos ctxt pred cs));
 
 end;
 
 
 (* position label *)
 
 val command_prefix = Markup.commandN ^ ".";
 
 fun markup_extern_label pos =
   Position.label_of pos |> Option.map (fn label =>
     (case try (unprefix command_prefix) label of
       SOME cmd => (Markup.keyword1, Long_Name.base_name cmd)
     | NONE => (Markup.empty, label)));
 
 fun print_label pos =
   (case markup_extern_label pos of
     NONE => ""
   | SOME (m, s) => Markup.markup m s);
 
 
 (* context tracing *)
 
 fun context_type (Context.Theory _) = "theory"
   | context_type (Context.Proof ctxt) =
       if can Local_Theory.assert ctxt then "local_theory" else "Proof.context";
 
 fun print_context_tracing (context, pos) =
   context_type context ^ (case print_label pos of "" => "" | s => " " ^ s) ^ Position.here pos;
 
 end;
diff --git a/src/Pure/PIDE/markup.ML b/src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML
+++ b/src/Pure/PIDE/markup.ML
@@ -1,878 +1,877 @@
 (*  Title:      Pure/PIDE/markup.ML
     Author:     Makarius
 
 Quasi-abstract markup elements.
 *)
 
 signature MARKUP =
 sig
   type T = string * Properties.T
   val empty: T
   val is_empty: T -> bool
   val properties: Properties.T -> T -> T
   val nameN: string val name: string -> T -> T
+  val name_proper: string -> Properties.T
   val xnameN: string val xname: string -> T -> T
-  val kindN: string
+  val kindN: string val kind: string -> T -> T
+  val kind_proper: string -> Properties.T
   val serialN: string
   val serial_properties: int -> Properties.T
   val instanceN: string
   val meta_titleN: string val meta_title: T
   val meta_creatorN: string val meta_creator: T
   val meta_contributorN: string val meta_contributor: T
   val meta_dateN: string val meta_date: T
   val meta_licenseN: string val meta_license: T
   val meta_descriptionN: string val meta_description: T
   val languageN: string
   val symbolsN: string
   val delimitedN: string
   val is_delimited: Properties.T -> bool
   val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T
   val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T
   val language_Isar: bool -> T
   val language_method: T
   val language_attribute: T
   val language_sort: bool -> T
   val language_type: bool -> T
   val language_term: bool -> T
   val language_prop: bool -> T
   val language_ML: bool -> T
   val language_SML: bool -> T
   val language_document: bool -> T
   val language_document_marker: T
   val language_antiquotation: T
   val language_text: bool -> T
   val language_verbatim: bool -> T
   val language_latex: bool -> T
   val language_rail: T
   val language_path: bool -> T
   val language_url: bool -> T
   val language_mixfix: T
   val bindingN: string val binding: T
   val entityN: string val entity: string -> string -> T
   val defN: string
   val refN: string
   val completionN: string val completion: T
   val no_completionN: string val no_completion: T
   val updateN: string val update: T
   val lineN: string
   val end_lineN: string
   val offsetN: string
   val end_offsetN: string
   val labelN: string
   val fileN: string
   val idN: string
   val positionN: string val position: T
   val position_properties: string list
   val position_property: Properties.entry -> bool
   val def_name: string -> string
   val expressionN: string val expression: string -> T
   val citationN: string val citation: string -> T
   val pathN: string val path: string -> T
   val export_pathN: string val export_path: string -> T
   val urlN: string val url: string -> T
   val docN: string val doc: string -> T
   val toolN: string val tool: string -> T
   val markupN: string
   val consistentN: string
   val unbreakableN: string
   val block_properties: string list
   val indentN: string
   val widthN: string
   val blockN: string val block: bool -> int -> T
   val breakN: string val break: int -> int -> T
   val fbreakN: string val fbreak: T
   val itemN: string val item: T
   val wordsN: string val words: T
   val hiddenN: string val hidden: T
   val deleteN: string val delete: T
   val load_commandN: string
   val bash_functionN: string
   val bibtex_entryN: string
   val scala_functionN: string
   val system_optionN: string
   val sessionN: string
   val theoryN: string
   val classN: string
   val localeN: string
   val bundleN: string
   val type_nameN: string
   val constantN: string
   val axiomN: string
   val factN: string
   val oracleN: string
   val fixedN: string val fixed: string -> T
   val caseN: string val case_: string -> T
   val dynamic_factN: string val dynamic_fact: string -> T
   val literal_factN: string val literal_fact: string -> T
   val attributeN: string
   val methodN: string
   val method_modifierN: string
   val tfreeN: string val tfree: T
   val tvarN: string val tvar: T
   val freeN: string val free: T
   val skolemN: string val skolem: T
   val boundN: string val bound: T
   val varN: string val var: T
   val numeralN: string val numeral: T
   val literalN: string val literal: T
   val delimiterN: string val delimiter: T
   val inner_stringN: string val inner_string: T
   val inner_cartoucheN: string val inner_cartouche: T
   val token_rangeN: string val token_range: T
   val sortingN: string val sorting: T
   val typingN: string val typing: T
   val class_parameterN: string val class_parameter: T
   val ML_keyword1N: string val ML_keyword1: T
   val ML_keyword2N: string val ML_keyword2: T
   val ML_keyword3N: string val ML_keyword3: T
   val ML_delimiterN: string val ML_delimiter: T
   val ML_tvarN: string val ML_tvar: T
   val ML_numeralN: string val ML_numeral: T
   val ML_charN: string val ML_char: T
   val ML_stringN: string val ML_string: T
   val ML_commentN: string val ML_comment: T
   val ML_defN: string
   val ML_openN: string
   val ML_structureN: string
   val ML_typingN: string val ML_typing: T
   val ML_breakpointN: string val ML_breakpoint: int -> T
   val antiquotedN: string val antiquoted: T
   val antiquoteN: string val antiquote: T
   val file_typeN: string
   val antiquotationN: string
   val ML_antiquotationN: string
   val document_antiquotationN: string
   val document_antiquotation_optionN: string
   val prismjs_languageN: string
   val raw_textN: string val raw_text: T
   val plain_textN: string val plain_text: T
   val paragraphN: string val paragraph: T
   val text_foldN: string val text_fold: T
   val document_markerN: string val document_marker: T
   val document_tagN: string val document_tag: string -> T
   val document_latexN: string val document_latex: T
   val latex_outputN: string val latex_output: T
   val latex_macro0N: string val latex_macro0: string -> T
   val latex_macroN: string val latex_macro: string -> T
   val latex_environmentN: string val latex_environment: string -> T
   val latex_headingN: string val latex_heading: string -> T
   val latex_bodyN: string val latex_body: string -> T
   val latex_citeN: string val latex_cite: {kind: string, citations: string} -> T
   val latex_index_itemN: string val latex_index_item: T
   val latex_index_entryN: string val latex_index_entry: string -> T
   val latex_delimN: string val latex_delim: string -> T
   val latex_tagN: string val latex_tag: string -> T
   val optional_argumentN: string val optional_argument: string -> T -> T
   val markdown_paragraphN: string val markdown_paragraph: T
   val markdown_itemN: string val markdown_item: T
   val markdown_bulletN: string val markdown_bullet: int -> T
   val markdown_listN: string val markdown_list: string -> T
   val itemizeN: string
   val enumerateN: string
   val descriptionN: string
   val inputN: string val input: bool -> Properties.T -> T
   val command_keywordN: string val command_keyword: T
   val command_spanN: string val command_span: {name: string, kind: string} -> T
   val commandN: string val command_properties: T -> T
   val keywordN: string val keyword_properties: T -> T
   val stringN: string val string: T
   val alt_stringN: string val alt_string: T
   val verbatimN: string val verbatim: T
   val cartoucheN: string val cartouche: T
   val commentN: string val comment: T
   val keyword1N: string val keyword1: T
   val keyword2N: string val keyword2: T
   val keyword3N: string val keyword3: T
   val quasi_keywordN: string val quasi_keyword: T
   val improperN: string val improper: T
   val operatorN: string val operator: T
   val comment1N: string val comment1: T
   val comment2N: string val comment2: T
   val comment3N: string val comment3: T
   val elapsedN: string
   val cpuN: string
   val gcN: string
   val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T
   val parse_command_timing_properties:
     Properties.T -> ({file: string, offset: int, name: string} * Time.time) option
   val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T
   val command_indentN: string val command_indent: int -> T
   val goalN: string val goal: T
   val subgoalN: string val subgoal: string -> T
   val taskN: string
   val forkedN: string val forked: T
   val joinedN: string val joined: T
   val runningN: string val running: T
   val finishedN: string val finished: T
   val failedN: string val failed: T
   val canceledN: string val canceled: T
   val initializedN: string val initialized: T
   val finalizedN: string val finalized: T
   val consolidatingN: string val consolidating: T
   val consolidatedN: string val consolidated: T
   val exec_idN: string
   val initN: string
   val statusN: string val status: T
   val resultN: string val result: T
   val writelnN: string val writeln: T
   val stateN: string val state: T
   val informationN: string val information: T
   val tracingN: string val tracing: T
   val warningN: string val warning: T
   val legacyN: string val legacy: T
   val errorN: string val error: T
   val systemN: string val system: T
   val protocolN: string
   val reportN: string val report: T
   val no_reportN: string val no_report: T
   val badN: string val bad: unit -> T
   val intensifyN: string val intensify: T
   val countN: string
   val ML_profiling_entryN: string
   val ML_profiling_entry: {name: string, count: int} -> T
   val ML_profilingN: string
   val ML_profiling: string -> T
   val browserN: string
   val graphviewN: string
   val theory_exportsN: string
   val sendbackN: string
   val paddingN: string
   val padding_line: Properties.entry
   val padding_command: Properties.entry
   val dialogN: string val dialog: serial -> string -> T
   val jedit_actionN: string
   val function: string -> Properties.entry
   val ML_statistics: {pid: int, stats_dir: string} -> Properties.T
   val commands_accepted: Properties.T
   val assign_update: Properties.T
   val removed_versions: Properties.T
   val invoke_scala: string -> string -> Properties.T
   val cancel_scala: string -> Properties.T
   val task_statistics: Properties.entry
   val command_timing: Properties.entry
   val theory_timing: Properties.entry
   val session_timing: Properties.entry
   val loading_theory: string -> Properties.T
   val build_session_finished: Properties.T
   val print_operations: Properties.T
   val exportN: string
   type export_args =
    {id: string option,
     serial: serial,
     theory_name: string,
     name: string,
     executable: bool,
     compress: bool,
     strict: bool}
   val export: export_args -> Properties.T
   val debugger_state: string -> Properties.T
   val debugger_output: string -> Properties.T
   val simp_trace_panelN: string
   val simp_trace_logN: string
   val simp_trace_stepN: string
   val simp_trace_recurseN: string
   val simp_trace_hintN: string
   val simp_trace_ignoreN: string
   val simp_trace_cancel: serial -> Properties.T
   type output = Output.output * Output.output
   val no_output: output
   val add_mode: string -> (T -> output) -> unit
   val output: T -> output
   val enclose: T -> Output.output -> Output.output
   val markup: T -> string -> string
   val markups: T list -> string -> string
   val markup_only: T -> string
   val markup_report: string -> string
 end;
 
 structure Markup: MARKUP =
 struct
 
 (** markup elements **)
 
 (* basic markup *)
 
 type T = string * Properties.T;
 
 val empty = ("", []);
 
 fun is_empty ("", _) = true
   | is_empty _ = false;
 
 
 fun properties more_props ((elem, props): T) =
   (elem, fold_rev Properties.put more_props props);
 
 fun markup_elem name = (name, (name, []): T);
 fun markup_string name prop = (name, fn s => (name, [(prop, s)]): T);
 fun markup_int name prop = (name, fn i => (name, [(prop, Value.print_int i)]): T);
 
 
 (* misc properties *)
 
 val nameN = "name";
 fun name a = properties [(nameN, a)];
+val name_proper = Properties.make_string nameN;
 
 val xnameN = "xname";
 fun xname a = properties [(xnameN, a)];
 
 val kindN = "kind";
+fun kind a = properties [(kindN, a)];
+val kind_proper = Properties.make_string kindN;
 
 val serialN = "serial";
 fun serial_properties i = [(serialN, Value.print_int i)];
 
 val instanceN = "instance";
 
 
 (* meta data -- see https://www.dublincore.org/specifications/dublin-core/dcmi-terms *)
 
 val (meta_titleN, meta_title) = markup_elem "meta_title";
 val (meta_creatorN, meta_creator) = markup_elem "meta_creator";
 val (meta_contributorN, meta_contributor) = markup_elem "meta_contributor";
 val (meta_dateN, meta_date) = markup_elem "meta_date";
 val (meta_licenseN, meta_license) = markup_elem "meta_license";
 val (meta_descriptionN, meta_description) = markup_elem "meta_description";
 
 
 (* embedded languages *)
 
 val languageN = "language";
 val symbolsN = "symbols";
 val antiquotesN = "antiquotes";
 val delimitedN = "delimited"
 
 fun is_delimited props =
   Properties.get props delimitedN = SOME "true";
 
 fun language {name, symbols, antiquotes, delimited} =
   (languageN,
    [(nameN, name),
     (symbolsN, Value.print_bool symbols),
     (antiquotesN, Value.print_bool antiquotes),
     (delimitedN, Value.print_bool delimited)]);
 
 fun language' {name, symbols, antiquotes} delimited =
   language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited};
 
 val language_Isar = language' {name = "Isar", symbols = true, antiquotes = false};
 val language_method =
   language {name = "method", symbols = true, antiquotes = false, delimited = false};
 val language_attribute =
   language {name = "attribute", symbols = true, antiquotes = false, delimited = false};
 val language_sort = language' {name = "sort", symbols = true, antiquotes = false};
 val language_type = language' {name = "type", symbols = true, antiquotes = false};
 val language_term = language' {name = "term", symbols = true, antiquotes = false};
 val language_prop = language' {name = "prop", symbols = true, antiquotes = false};
 val language_ML = language' {name = "ML", symbols = false, antiquotes = true};
 val language_SML = language' {name = "SML", symbols = false, antiquotes = false};
 val language_document = language' {name = "document", symbols = false, antiquotes = true};
 val language_document_marker =
   language {name = "document_marker", symbols = true, antiquotes = true, delimited = true};
 val language_antiquotation =
   language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
 val language_text = language' {name = "text", symbols = true, antiquotes = false};
 val language_verbatim = language' {name = "verbatim_text", symbols = true, antiquotes = false};
 val language_latex = language' {name = "latex", symbols = false, antiquotes = false};
 val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true};
 val language_path = language' {name = "path", symbols = false, antiquotes = false};
 val language_url = language' {name = "url", symbols = false, antiquotes = false};
 val language_mixfix =
   language {name = "mixfix_annotation", symbols = true, antiquotes = false, delimited = true};
 
 
 (* formal entities *)
 
 val (bindingN, binding) = markup_elem "binding";
 
 val entityN = "entity";
-fun entity kind name =
-  (entityN,
-    (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)]));
+fun entity kind name = (entityN, name_proper name @ kind_proper kind);
 
 val defN = "def";
 val refN = "ref";
 
 
 (* completion *)
 
 val (completionN, completion) = markup_elem "completion";
 val (no_completionN, no_completion) = markup_elem "no_completion";
 
 val (updateN, update) = markup_elem "update";
 
 
 (* position *)
 
 val lineN = "line";
 val end_lineN = "end_line";
 
 val offsetN = "offset";
 val end_offsetN = "end_offset";
 
 val labelN = "label";
 val fileN = "file";
 val idN = "id";
 
 val (positionN, position) = markup_elem "position";
 
 val position_properties = [lineN, offsetN, end_offsetN, labelN, fileN, idN];
 fun position_property (entry: Properties.entry) = member (op =) position_properties (#1 entry);
 
 
 (* position "def" names *)
 
 fun make_def a = "def_" ^ a;
 
 val def_names = Symtab.make (map (fn a => (a, make_def a)) position_properties);
 
 fun def_name a =
   (case Symtab.lookup def_names a of
     SOME b => b
   | NONE => make_def a);
 
 
 (* expression *)
 
 val expressionN = "expression";
-fun expression kind = (expressionN, if kind = "" then [] else [(kindN, kind)]);
+fun expression kind = (expressionN, kind_proper kind);
 
 
 (* citation *)
 
 val (citationN, citation) = markup_string "citation" nameN;
 
 
 (* external resources *)
 
 val (pathN, path) = markup_string "path" nameN;
 val (export_pathN, export_path) = markup_string "export_path" nameN;
 val (urlN, url) = markup_string "url" nameN;
 val (docN, doc) = markup_string "doc" nameN;
 val (toolN, tool) = markup_string "tool" nameN;
 
 
 (* pretty printing *)
 
 val markupN = "markup";
 val consistentN = "consistent";
 val unbreakableN = "unbreakable";
 val indentN = "indent";
 
 val block_properties = [markupN, consistentN, unbreakableN, indentN];
 
 val widthN = "width";
 
 val blockN = "block";
 fun block c i =
   (blockN,
     (if c then [(consistentN, Value.print_bool c)] else []) @
     (if i <> 0 then [(indentN, Value.print_int i)] else []));
 
 val breakN = "break";
 fun break w i =
   (breakN,
     (if w <> 0 then [(widthN, Value.print_int w)] else []) @
     (if i <> 0 then [(indentN, Value.print_int i)] else []));
 
 val (fbreakN, fbreak) = markup_elem "fbreak";
 
 val (itemN, item) = markup_elem "item";
 
 
 (* text properties *)
 
 val (wordsN, words) = markup_elem "words";
 
 val (hiddenN, hidden) = markup_elem "hidden";
 
 val (deleteN, delete) = markup_elem "delete";
 
 
 (* misc entities *)
 
 val load_commandN = "load_command";
 val bash_functionN = "bash_function";
 val bibtex_entryN = "bibtex_entry";
 val scala_functionN = "scala_function";
 val system_optionN = "system_option";
 
 val sessionN = "session";
 
 val theoryN = "theory";
 val classN = "class";
 val localeN = "locale";
 val bundleN = "bundle";
 val type_nameN = "type_name";
 val constantN = "constant";
 val axiomN = "axiom";
 val factN = "fact";
 val oracleN = "oracle";
 
 val (fixedN, fixed) = markup_string "fixed" nameN;
 val (caseN, case_) = markup_string "case" nameN;
 val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
 val (literal_factN, literal_fact) = markup_string "literal_fact" nameN;
 
 val attributeN = "attribute";
 val methodN = "method";
 val method_modifierN = "method_modifier";
 
 
 (* inner syntax *)
 
 val (tfreeN, tfree) = markup_elem "tfree";
 val (tvarN, tvar) = markup_elem "tvar";
 val (freeN, free) = markup_elem "free";
 val (skolemN, skolem) = markup_elem "skolem";
 val (boundN, bound) = markup_elem "bound";
 val (varN, var) = markup_elem "var";
 val (numeralN, numeral) = markup_elem "numeral";
 val (literalN, literal) = markup_elem "literal";
 val (delimiterN, delimiter) = markup_elem "delimiter";
 val (inner_stringN, inner_string) = markup_elem "inner_string";
 val (inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche";
 
 val (token_rangeN, token_range) = markup_elem "token_range";
 
 val (sortingN, sorting) = markup_elem "sorting";
 val (typingN, typing) = markup_elem "typing";
 val (class_parameterN, class_parameter) = markup_elem "class_parameter";
 
 
 (* ML *)
 
 val (ML_keyword1N, ML_keyword1) = markup_elem "ML_keyword1";
 val (ML_keyword2N, ML_keyword2) = markup_elem "ML_keyword2";
 val (ML_keyword3N, ML_keyword3) = markup_elem "ML_keyword3";
 val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
 val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
 val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
 val (ML_charN, ML_char) = markup_elem "ML_char";
 val (ML_stringN, ML_string) = markup_elem "ML_string";
 val (ML_commentN, ML_comment) = markup_elem "ML_comment";
 
 val ML_defN = "ML_def";
 val ML_openN = "ML_open";
 val ML_structureN = "ML_structure";
 val (ML_typingN, ML_typing) = markup_elem "ML_typing";
 
 val (ML_breakpointN, ML_breakpoint) = markup_int "ML_breakpoint" serialN;
 
 
 (* antiquotations *)
 
 val (antiquotedN, antiquoted) = markup_elem "antiquoted";
 val (antiquoteN, antiquote) = markup_elem "antiquote";
 
 val file_typeN = "file_type";
 val antiquotationN = "antiquotation";
 val ML_antiquotationN = "ML_antiquotation";
 val document_antiquotationN = "document_antiquotation";
 val document_antiquotation_optionN = "document_antiquotation_option";
 
 
 (* document text *)
 
 val prismjs_languageN = "prismjs_language";
 
 val (raw_textN, raw_text) = markup_elem "raw_text";
 val (plain_textN, plain_text) = markup_elem "plain_text";
 
 val (paragraphN, paragraph) = markup_elem "paragraph";
 val (text_foldN, text_fold) = markup_elem "text_fold";
 
 val (document_markerN, document_marker) = markup_elem "document_marker";
 val (document_tagN, document_tag) = markup_string "document_tag" nameN;
 
 
 (* LaTeX *)
 
 val (document_latexN, document_latex) = markup_elem "document_latex";
 
 val (latex_outputN, latex_output) = markup_elem "latex_output";
 val (latex_macro0N, latex_macro0) = markup_string "latex_macro0" nameN;
 val (latex_macroN, latex_macro) = markup_string "latex_macro" nameN;
 val (latex_environmentN, latex_environment) = markup_string "latex_environment" nameN;
 val (latex_headingN, latex_heading) = markup_string "latex_heading" kindN;
 val (latex_bodyN, latex_body) = markup_string "latex_body" kindN;
 val (latex_citeN, _) = markup_elem "latex_cite";
 fun latex_cite {kind, citations} =
-  (latex_citeN,
-    (if kind = "" then [] else [(kindN, kind)]) @
-    (if citations = "" then [] else [("citations", citations)]));
+  (latex_citeN, kind_proper kind @ Properties.make_string "citations" citations);
 val (latex_index_itemN, latex_index_item) = markup_elem "latex_index_item";
 val (latex_index_entryN, latex_index_entry) = markup_string "latex_index_entry" kindN;
 val (latex_delimN, latex_delim) = markup_string "latex_delim" nameN;
 val (latex_tagN, latex_tag) = markup_string "latex_tag" nameN;
 
 val optional_argumentN = "optional_argument";
 fun optional_argument arg = properties [(optional_argumentN, arg)];
 
 
 (* Markdown document structure *)
 
 val (markdown_paragraphN, markdown_paragraph) = markup_elem "markdown_paragraph";
 val (markdown_itemN, markdown_item) = markup_elem "markdown_item";
 val (markdown_bulletN, markdown_bullet) = markup_int "markdown_bullet" "depth";
 val (markdown_listN, markdown_list) = markup_string "markdown_list" kindN;
 
 val itemizeN = "itemize";
 val enumerateN = "enumerate";
 val descriptionN = "description";
 
 
 (* formal input *)
 
 val inputN = "input";
 fun input delimited props = (inputN, (delimitedN, Value.print_bool delimited) :: props);
 
 
 (* outer syntax *)
 
 val (command_keywordN, command_keyword) = markup_elem "command_keyword";
 
 val command_spanN = "command_span";
-fun command_span {name, kind} : T =
-  (command_spanN,
-    (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)]));
+fun command_span {name, kind} : T = (command_spanN, name_proper name @ kind_proper kind);
 
 val commandN = "command"; val command_properties = properties [(kindN, commandN)];
 val keywordN = "keyword"; val keyword_properties = properties [(kindN, keywordN)];
 
 val (keyword1N, keyword1) = markup_elem "keyword1";
 val (keyword2N, keyword2) = markup_elem "keyword2";
 val (keyword3N, keyword3) = markup_elem "keyword3";
 val (quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword";
 val (improperN, improper) = markup_elem "improper";
 val (operatorN, operator) = markup_elem "operator";
 val (stringN, string) = markup_elem "string";
 val (alt_stringN, alt_string) = markup_elem "alt_string";
 val (verbatimN, verbatim) = markup_elem "verbatim";
 val (cartoucheN, cartouche) = markup_elem "cartouche";
 val (commentN, comment) = markup_elem "comment";
 
 
 (* comments *)
 
 val (comment1N, comment1) = markup_elem "comment1";
 val (comment2N, comment2) = markup_elem "comment2";
 val (comment3N, comment3) = markup_elem "comment3";
 
 
 (* timing *)
 
 val elapsedN = "elapsed";
 val cpuN = "cpu";
 val gcN = "gc";
 
 fun timing_properties {elapsed, cpu, gc} =
  [(elapsedN, Value.print_time elapsed),
   (cpuN, Value.print_time cpu),
   (gcN, Value.print_time gc)];
 
 val timingN = "timing";
 fun timing t = (timingN, timing_properties t);
 
 
 (* command timing *)
 
 fun parse_command_timing_properties props =
   (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of
     (SOME file, SOME offset, SOME name) =>
       SOME ({file = file, offset = Value.parse_int offset, name = name},
         Properties.get_seconds props elapsedN)
   | _ => NONE);
 
 
 (* indentation *)
 
 val (command_indentN, command_indent) = markup_int "command_indent" indentN;
 
 
 (* goals *)
 
 val (goalN, goal) = markup_elem "goal";
 val (subgoalN, subgoal) = markup_string "subgoal" nameN;
 
 
 (* command status *)
 
 val taskN = "task";
 
 val (forkedN, forked) = markup_elem "forked";
 val (joinedN, joined) = markup_elem "joined";
 val (runningN, running) = markup_elem "running";
 val (finishedN, finished) = markup_elem "finished";
 val (failedN, failed) = markup_elem "failed";
 val (canceledN, canceled) = markup_elem "canceled";
 val (initializedN, initialized) = markup_elem "initialized";
 val (finalizedN, finalized) = markup_elem "finalized";
 val (consolidatingN, consolidating) = markup_elem "consolidating";
 val (consolidatedN, consolidated) = markup_elem "consolidated";
 
 
 (* messages *)
 
 val exec_idN = "exec_id";
 
 val initN = "init";
 val (statusN, status) = markup_elem "status";
 val (resultN, result) = markup_elem "result";
 val (writelnN, writeln) = markup_elem "writeln";
 val (stateN, state) = markup_elem "state"
 val (informationN, information) = markup_elem "information";
 val (tracingN, tracing) = markup_elem "tracing";
 val (warningN, warning) = markup_elem "warning";
 val (legacyN, legacy) = markup_elem "legacy";
 val (errorN, error) = markup_elem "error";
 val (systemN, system) = markup_elem "system";
 val protocolN = "protocol";
 
 val (reportN, report) = markup_elem "report";
 val (no_reportN, no_report) = markup_elem "no_report";
 
 val badN = "bad";
 fun bad () = (badN, serial_properties (serial ()));
 
 val (intensifyN, intensify) = markup_elem "intensify";
 
 
 (* ML profiling *)
 
 val countN = "count";
 
 val ML_profiling_entryN = "ML_profiling_entry";
 fun ML_profiling_entry {name, count} =
   (ML_profiling_entryN, [(nameN, name), (countN, Value.print_int count)]);
 
 val (ML_profilingN, ML_profiling) = markup_string "ML_profiling" kindN;
 
 
 (* active areas *)
 
 val browserN = "browser"
 val graphviewN = "graphview";
 val theory_exportsN = "theory_exports";
 
 val sendbackN = "sendback";
 val paddingN = "padding";
 val padding_line = (paddingN, "line");
 val padding_command = (paddingN, "command");
 
 val dialogN = "dialog";
 fun dialog i result = (dialogN, [(serialN, Value.print_int i), (resultN, result)]);
 
 val jedit_actionN = "jedit_action";
 
 
 (* protocol message functions *)
 
 fun function name = ("function", name);
 
 fun ML_statistics {pid, stats_dir} =
   [function "ML_statistics", ("pid", Value.print_int pid), ("stats_dir", stats_dir)];
 
 val commands_accepted = [function "commands_accepted"];
 
 val assign_update = [function "assign_update"];
 val removed_versions = [function "removed_versions"];
 
 fun invoke_scala name id = [function "invoke_scala", (nameN, name), (idN, id)];
 
 fun cancel_scala id = [function "cancel_scala", (idN, id)];
 
 val task_statistics = function "task_statistics";
 
 val command_timing = function "command_timing";
 
 val theory_timing = function "theory_timing";
 
 val session_timing = function "session_timing";
 
 fun loading_theory name = [function "loading_theory", (nameN, name)];
 
 val build_session_finished = [function "build_session_finished"];
 
 val print_operations = [function "print_operations"];
 
 
 (* export *)
 
 val exportN = "export";
 
 type export_args =
  {id: string option,
   serial: serial,
   theory_name: string,
   name: string,
   executable: bool,
   compress: bool,
   strict: bool};
 
 fun export ({id, serial, theory_name, name, executable, compress, strict}: export_args) =
  [function exportN,
   (idN, the_default "" id),
   (serialN, Value.print_int serial),
   ("theory_name", theory_name),
   (nameN, name),
   ("executable", Value.print_bool executable),
   ("compress", Value.print_bool compress),
   ("strict", Value.print_bool strict)];
 
 
 (* debugger *)
 
 fun debugger_state name = [function "debugger_state", (nameN, name)];
 fun debugger_output name = [function "debugger_output", (nameN, name)];
 
 
 (* simplifier trace *)
 
 val simp_trace_panelN = "simp_trace_panel";
 
 val simp_trace_logN = "simp_trace_log";
 val simp_trace_stepN = "simp_trace_step";
 val simp_trace_recurseN = "simp_trace_recurse";
 val simp_trace_hintN = "simp_trace_hint";
 val simp_trace_ignoreN = "simp_trace_ignore";
 
 fun simp_trace_cancel i = [function "simp_trace_cancel", (serialN, Value.print_int i)];
 
 
 
 (** print mode operations **)
 
 type output = Output.output * Output.output;
 
 val no_output = ("", "");
 
 local
   val default = {output = Output_Primitives.markup_fn};
   val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
 in
   fun add_mode name output =
     Synchronized.change modes (fn tab =>
       (if not (Symtab.defined tab name) then ()
        else Output.warning ("Redefining markup mode " ^ quote name);
        Symtab.update (name, {output = output}) tab));
   fun get_mode () =
     the_default default
       (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
 end;
 
 fun output m = if is_empty m then no_output else #output (get_mode ()) m;
 
 val enclose = output #-> Library.enclose;
 
 fun markup m =
   let val (bg, en) = output m
   in Library.enclose (Output.escape bg) (Output.escape en) end;
 
 val markups = fold_rev markup;
 
 fun markup_only m = markup m "";
 
 fun markup_report "" = ""
   | markup_report txt = markup report txt;
 
 end;
diff --git a/src/Pure/Thy/bibtex.ML b/src/Pure/Thy/bibtex.ML
--- a/src/Pure/Thy/bibtex.ML
+++ b/src/Pure/Thy/bibtex.ML
@@ -1,134 +1,134 @@
 (*  Title:      Pure/Thy/bibtex.ML
     Author:     Makarius
 
 BibTeX support.
 *)
 
 signature BIBTEX =
 sig
   val check_database:
     Position.T -> string -> (string * Position.T) list * (string * Position.T) list
   val check_database_output: Position.T -> string -> unit
   val check_bibtex_entry: Proof.context -> string * Position.T -> unit
   val cite_macro: string Config.T
   val cite_antiquotation: binding -> (Proof.context -> string) -> theory -> theory
 end;
 
 structure Bibtex: BIBTEX =
 struct
 
 (* check database *)
 
 type message = string * Position.T;
 
 fun check_database pos0 database =
   \<^scala>\<open>bibtex_check_database\<close> database
   |> YXML.parse_body
   |> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end
   |> (apply2 o map o apsnd)
       (fn pos => Position.of_properties (pos @ Position.properties_of pos0));
 
 fun check_database_output pos0 database =
   let val (errors, warnings) = check_database pos0 database in
     errors |> List.app (fn (msg, pos) =>
       Output.error_message ("Bibtex error" ^ Position.here pos ^ ":\n  " ^ msg));
     warnings |> List.app (fn (msg, pos) =>
       warning ("Bibtex warning" ^ Position.here pos ^ ":\n  " ^ msg))
   end;
 
 
 (* check bibtex entry *)
 
 fun check_bibtex_entry ctxt (name, pos) =
   let
     fun warn () =
       if Context_Position.is_visible ctxt then
         warning ("Unknown session context: cannot check Bibtex entry " ^
           quote name ^ Position.here pos)
       else ();
     fun decode yxml =
       let
         val props = XML.Decode.properties (YXML.parse_body yxml);
-        val name = the_default "" (Properties.get props Markup.nameN);
+        val name = Properties.get_string props Markup.nameN;
         val pos = Position.of_properties props;
       in (name, pos) end;
   in
     if name = "*" then ()
     else
       (case Position.id_of pos of
         NONE => warn ()
       | SOME id =>
           (case \<^scala>\<open>bibtex_session_entries\<close> [id] of
             [] => warn ()
           | _ :: entries =>
               Completion.check_entity Markup.bibtex_entryN (map decode entries)
                 ctxt (name, pos) |> ignore))
   end;
 
 
 (* document antiquotations *)
 
 val cite_macro = Attrib.setup_config_string \<^binding>\<open>cite_macro\<close> (K "");
 fun get_cite_macro ctxt = Config.get ctxt cite_macro;
 
 val _ =
   Theory.setup (Document_Antiquotation.setup_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro));
 
 
 local
 
 val parse_citations = Parse.and_list1 (Parse.position Parse.name);
 
 fun cite_command ctxt get_kind ((opt_loc, citations), macro_name) =
   let
     val loc = the_default Input.empty opt_loc;
     val _ = Context_Position.reports ctxt (Document_Output.document_reports loc);
     val _ = List.app (check_bibtex_entry ctxt) citations;
 
     val kind = if macro_name = "" then get_kind ctxt else macro_name;
     val location = Document_Output.output_document ctxt {markdown = false} loc;
   in Latex.cite {kind = kind, citations = citations, location = location} end;
 
 fun cite_command_old ctxt get_kind args =
   let
     val _ =
       if Context_Position.is_visible ctxt then
         legacy_feature ("Old antiquotation syntax, better use \"isabelle update -u cite\"" ^
           Position.here_list (map snd (snd args)))
       else ();
   in cite_command ctxt get_kind (args, "") end;
 
 val cite_keywords =
   Thy_Header.bootstrap_keywords
   |> Keyword.add_keywords (map (fn a => ((a, Position.none), Keyword.no_spec)) ["in", "using"]);
 
 fun cite_command_embedded ctxt get_kind input =
   let
     val parser =
       Scan.option (Parse.embedded_input --| Parse.$$$ "in") -- parse_citations --
         Scan.optional (Parse.$$$ "using" |-- Parse.!!! Parse.name) "";
     val args = Parse.read_embedded ctxt cite_keywords parser input;
   in cite_command ctxt get_kind args end;
 
 fun cite_command_parser get_kind =
   Scan.option Args.cartouche_input -- parse_citations
     >> (fn args => fn ctxt => cite_command_old ctxt get_kind args) ||
   Parse.embedded_input
     >> (fn arg => fn ctxt => cite_command_embedded ctxt get_kind arg);
 
 in
 
 fun cite_antiquotation binding get_kind =
   Document_Output.antiquotation_raw binding (Scan.lift (cite_command_parser get_kind))
     (fn ctxt => fn cmd => cmd ctxt);
 
 end;
 
 val _ =
   Theory.setup
    (cite_antiquotation \<^binding>\<open>cite\<close> get_cite_macro #>
     cite_antiquotation \<^binding>\<open>nocite\<close> (K "nocite") #>
     cite_antiquotation \<^binding>\<open>citet\<close> (K "citet") #>
     cite_antiquotation \<^binding>\<open>citep\<close> (K "citep"));
 
 end;
diff --git a/src/Pure/context.ML b/src/Pure/context.ML
--- a/src/Pure/context.ML
+++ b/src/Pure/context.ML
@@ -1,836 +1,840 @@
 (*  Title:      Pure/context.ML
     Author:     Markus Wenzel, TU Muenchen
 
 Generic theory contexts with unique identity, arbitrarily typed data,
 monotonic development graph and history support.  Generic proof
 contexts with arbitrarily typed data.
 
 Firm naming conventions:
    thy, thy', thy1, thy2: theory
    ctxt, ctxt', ctxt1, ctxt2: Proof.context
    context: Context.generic
 *)
 
 signature BASIC_CONTEXT =
 sig
   type theory
   exception THEORY of string * theory list
   structure Proof: sig type context end
   structure Proof_Context:
   sig
     val theory_of: Proof.context -> theory
     val init_global: theory -> Proof.context
     val get_global: {long: bool} -> theory -> string -> Proof.context
   end
 end;
 
 signature CONTEXT =
 sig
   include BASIC_CONTEXT
   (*theory data*)
   type data_kind = int
   val data_kinds: unit -> (data_kind * Position.T) list
   (*theory context*)
   type id = int
   type theory_id
   val theory_id: theory -> theory_id
   val data_timing: bool Unsynchronized.ref
   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
   val theory_id_ord: theory_id ord
   val theory_id_name: {long: bool} -> theory_id -> string
   val theory_long_name: theory -> string
   val theory_base_name: theory -> string
   val theory_name: {long: bool} -> theory -> string
   val theory_identifier: theory -> id
   val PureN: string
   val pretty_thy: theory -> Pretty.T
   val pretty_abbrev_thy: theory -> Pretty.T
   val get_theory: {long: bool} -> theory -> string -> theory
   val eq_thy_id: theory_id * theory_id -> bool
   val eq_thy: theory * theory -> bool
   val proper_subthy_id: theory_id * theory_id -> bool
   val proper_subthy: theory * theory -> bool
   val subthy_id: theory_id * theory_id -> bool
   val subthy: theory * theory -> bool
   val join_thys: theory list -> theory
   val begin_thy: string -> theory list -> theory
   val finish_thy: theory -> theory
   val theory_data_sizeof1: theory -> (Position.T * int) list
   (*proof context*)
   val raw_transfer: theory -> Proof.context -> Proof.context
   (*certificate*)
   datatype certificate = Certificate of theory | Certificate_Id of theory_id
   val certificate_theory: certificate -> theory
   val certificate_theory_id: certificate -> theory_id
   val eq_certificate: certificate * certificate -> bool
   val join_certificate: certificate * certificate -> certificate
   val join_certificate_theory: theory * theory -> theory
   (*generic context*)
   datatype generic = Theory of theory | Proof of Proof.context
   val theory_tracing: bool Unsynchronized.ref
   val proof_tracing: bool Unsynchronized.ref
   val enabled_tracing: unit -> bool
   val finish_tracing: unit ->
    {contexts: (generic * Position.T) list,
     active_contexts: int,
     active_theories: int,
     active_proofs: int,
     total_contexts: int,
     total_theories: int,
     total_proofs: int}
   val cases: (theory -> 'a) -> (Proof.context -> 'a) -> generic -> 'a
   val mapping: (theory -> theory) -> (Proof.context -> Proof.context) -> generic -> generic
   val mapping_result: (theory -> 'a * theory) -> (Proof.context -> 'a * Proof.context) ->
     generic -> 'a * generic
   val the_theory: generic -> theory
   val the_proof: generic -> Proof.context
   val map_theory: (theory -> theory) -> generic -> generic
   val map_proof: (Proof.context -> Proof.context) -> generic -> generic
   val map_theory_result: (theory -> 'a * theory) -> generic -> 'a * generic
   val map_proof_result: (Proof.context -> 'a * Proof.context) -> generic -> 'a * generic
   val theory_map: (generic -> generic) -> theory -> theory
   val proof_map: (generic -> generic) -> Proof.context -> Proof.context
   val theory_of: generic -> theory  (*total*)
   val proof_of: generic -> Proof.context  (*total*)
   (*thread data*)
   val get_generic_context: unit -> generic option
   val put_generic_context: generic option -> unit
   val setmp_generic_context: generic option -> ('a -> 'b) -> 'a -> 'b
   val the_generic_context: unit -> generic
   val the_global_context: unit -> theory
   val the_local_context: unit -> Proof.context
   val >> : (generic -> generic) -> unit
   val >>> : (generic -> 'a * generic) -> 'a
 end;
 
 signature PRIVATE_CONTEXT =
 sig
   include CONTEXT
   structure Theory_Data:
   sig
     val declare: Position.T -> Any.T -> ((theory * Any.T) list -> Any.T) -> data_kind
     val get: data_kind -> (Any.T -> 'a) -> theory -> 'a
     val put: data_kind -> ('a -> Any.T) -> 'a -> theory -> theory
   end
   structure Proof_Data:
   sig
     val declare: (theory -> Any.T) -> data_kind
     val get: data_kind -> (Any.T -> 'a) -> Proof.context -> 'a
     val put: data_kind -> ('a -> Any.T) -> 'a -> Proof.context -> Proof.context
   end
 end;
 
 structure Context: PRIVATE_CONTEXT =
 struct
 
 (*** type definitions ***)
 
 (* context data *)
 
 (*private copy avoids potential conflict of table exceptions*)
 structure Datatab = Table(type key = int val ord = int_ord);
 
 type data_kind = int;
 val data_kind = Counter.make ();
 
 
 (* theory identity *)
 
 type id = int;
 val new_id = Counter.make ();
 
 abstype theory_id =
   Thy_Id of
    {id: id,         (*identifier*)
     ids: Intset.T,  (*cumulative identifiers -- symbolic body content*)
     name: string,   (*official theory name*)
     stage: int}     (*index for anonymous updates*)
 with
   fun rep_theory_id (Thy_Id args) = args;
   val make_theory_id = Thy_Id;
 end;
 
 
 (* theory allocation state *)
 
 type state = {stage: int} Synchronized.var;
 
 fun make_state () : state =
   Synchronized.var "Context.state" {stage = 0};
 
 fun next_stage (state: state) =
   Synchronized.change_result state (fn {stage} => (stage + 1, {stage = stage + 1}));
 
 
 (* theory and proof context *)
 
 datatype theory =
   Thy_Undef
 | Thy of
     (*allocation state*)
     state *
     (*identity*)
     {theory_id: theory_id,
      theory_token: theory Unsynchronized.ref,
      theory_token_pos: Position.T} *
     (*ancestry*)
     {parents: theory list,         (*immediate predecessors*)
      ancestors: theory list} *     (*all predecessors -- canonical reverse order*)
     (*data*)
     Any.T Datatab.table;           (*body content*)
 
 datatype proof =
   Prf_Undef
 | Prf of
     (*identity*)
     proof Unsynchronized.ref *  (*token*)
     Position.T *                (*token_pos*)
     theory *
     (*data*)
     Any.T Datatab.table;
 
 structure Proof = struct type context = proof end;
 
 datatype generic = Theory of theory | Proof of Proof.context;
 
 
 (* heap allocations *)
 
 val theory_tracing = Unsynchronized.ref false;
 val proof_tracing = Unsynchronized.ref false;
 
 fun enabled_tracing () = ! theory_tracing orelse ! proof_tracing;
 
 local
 
+val m = Integer.pow 18 2;
+
 fun cons_tokens var token =
-  Synchronized.change var (fn (n, tokens) => (n + 1, Weak.weak (SOME token) :: tokens));
+  Synchronized.change var (fn (n, tokens) =>
+    let val tokens' = if n mod m = 0 then filter Unsynchronized.weak_active tokens else tokens
+    in (n + 1, Weak.weak (SOME token) :: tokens') end);
 
 fun finish_tokens var =
   Synchronized.change_result var (fn (n, tokens) =>
     let
       val tokens' = filter Unsynchronized.weak_active tokens;
       val results = map_filter Unsynchronized.weak_peek tokens';
     in ((n, results), (n, tokens')) end);
 
 fun make_token guard var token0 =
   if ! guard then
     let
       val token = Unsynchronized.ref (! token0);
       val pos = Position.thread_data ();
       fun assign res = (token := res; cons_tokens var token; res);
     in (token, pos, assign) end
   else (token0, Position.none, I);
 
 val theory_tokens = Synchronized.var "theory_tokens" (0, []: theory Unsynchronized.weak_ref list);
 val proof_tokens = Synchronized.var "proof_tokens" (0, []: proof Unsynchronized.weak_ref list);
 
 val theory_token0 = Unsynchronized.ref Thy_Undef;
 val proof_token0 = Unsynchronized.ref Prf_Undef;
 
 in
 
 fun theory_token () = make_token theory_tracing theory_tokens theory_token0;
 fun proof_token () = make_token proof_tracing proof_tokens proof_token0;
 
 fun finish_tracing () =
   let
     val _ = ML_Heap.full_gc ();
     val (total_theories, token_theories) = finish_tokens theory_tokens;
     val (total_proofs, token_proofs) = finish_tokens proof_tokens;
 
     fun cons1 (thy as Thy (_, {theory_token_pos, ...}, _, _)) = cons (Theory thy, theory_token_pos)
       | cons1 _ = I;
     fun cons2 (ctxt as Prf (_, proof_token_pos, _, _)) = cons (Proof ctxt, proof_token_pos)
       | cons2 _ = I;
 
     val contexts = build (fold cons1 token_theories #> fold cons2 token_proofs);
     val active_theories = fold (fn (Theory _, _) => Integer.add 1 | _ => I) contexts 0;
     val active_proofs = fold (fn (Proof _, _) => Integer.add 1 | _ => I) contexts 0;
   in
     {contexts = contexts,
      active_contexts = active_theories + active_proofs,
      active_theories = active_theories,
      active_proofs = active_proofs,
      total_contexts = total_theories + total_proofs,
      total_theories = total_theories,
      total_proofs = total_proofs}
   end;
 
 end;
 
 
 
 (*** theory operations ***)
 
 fun rep_theory (Thy args) = args;
 
 exception THEORY of string * theory list;
 
 val state_of = #1 o rep_theory;
 val theory_identity = #2 o rep_theory;
 val theory_id = #theory_id o theory_identity;
 val identity_of = rep_theory_id o theory_id;
 val ancestry_of = #3 o rep_theory;
 val data_of = #4 o rep_theory;
 
 fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
 
 fun stage_final stage = stage = 0;
 
 val theory_id_stage = #stage o rep_theory_id;
 val theory_id_final = stage_final o theory_id_stage;
 val theory_id_ord = int_ord o apply2 (#id o rep_theory_id);
 fun theory_id_name {long} thy_id =
   let val name = #name (rep_theory_id thy_id)
   in if long then name else Long_Name.base_name name end;
 
 val theory_long_name = #name o identity_of;
 val theory_base_name = Long_Name.base_name o theory_long_name;
 fun theory_name {long} = if long then theory_long_name else theory_base_name;
 val theory_identifier = #id o identity_of;
 
 val parents_of = #parents o ancestry_of;
 val ancestors_of = #ancestors o ancestry_of;
 
 
 (* names *)
 
 val PureN = "Pure";
 
 fun display_name thy_id =
   let
     val name = theory_id_name {long = false} thy_id;
     val final = theory_id_final thy_id;
   in if final then name else name ^ ":" ^ string_of_int (theory_id_stage thy_id) end;
 
 fun display_names thy =
   let
     val name = display_name (theory_id thy);
     val ancestor_names = map theory_long_name (ancestors_of thy);
   in rev (name :: ancestor_names) end;
 
 val pretty_thy = Pretty.str_list "{" "}" o display_names;
 
 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_thy);
 
 fun pretty_abbrev_thy thy =
   let
     val names = display_names thy;
     val n = length names;
     val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names;
   in Pretty.str_list "{" "}" abbrev end;
 
 fun get_theory long thy name =
   if theory_name long thy <> name then
     (case find_first (fn thy' => theory_name long thy' = name) (ancestors_of thy) of
       SOME thy' => thy'
     | NONE => error ("Unknown ancestor theory " ^ quote name))
   else if theory_id_final (theory_id thy) then thy
   else error ("Unfinished theory " ^ quote name);
 
 
 (* identity *)
 
 fun merge_ids thys =
   fold (identity_of #> (fn {id, ids, ...} => fn acc => Intset.merge (acc, ids) |> Intset.insert id))
     thys Intset.empty;
 
 val eq_thy_id = op = o apply2 (#id o rep_theory_id);
 val eq_thy = op = o apply2 (#id o identity_of);
 
 val proper_subthy_id = apply2 rep_theory_id #> (fn ({id, ...}, {ids, ...}) => Intset.member ids id);
 val proper_subthy = proper_subthy_id o apply2 theory_id;
 
 fun subthy_id p = eq_thy_id p orelse proper_subthy_id p;
 val subthy = subthy_id o apply2 theory_id;
 
 
 (* consistent ancestors *)
 
 fun eq_thy_consistent (thy1, thy2) =
   eq_thy (thy1, thy2) orelse
     (theory_base_name thy1 = theory_base_name thy2 andalso
       raise THEORY ("Duplicate theory name", [thy1, thy2]));
 
 fun extend_ancestors thy thys =
   if member eq_thy_consistent thys thy then
     raise THEORY ("Duplicate theory node", thy :: thys)
   else thy :: thys;
 
 val merge_ancestors = merge eq_thy_consistent;
 
 val eq_ancestry =
   apply2 ancestry_of #>
     (fn ({parents, ancestors}, {parents = parents', ancestors = ancestors'}) =>
       eq_list eq_thy (parents, parents') andalso eq_list eq_thy (ancestors, ancestors'));
 
 
 
 (** theory data **)
 
 (* data kinds and access methods *)
 
 val data_timing = Unsynchronized.ref false;
 
 local
 
 type kind =
  {pos: Position.T,
   empty: Any.T,
   merge: (theory * Any.T) list -> Any.T};
 
 val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
 
 fun the_kind k =
   (case Datatab.lookup (Synchronized.value kinds) k of
     SOME kind => kind
   | NONE => raise Fail "Invalid theory data identifier");
 
 in
 
 fun data_kinds () =
   Datatab.fold_rev (fn (k, {pos, ...}) => cons (k, pos)) (Synchronized.value kinds) [];
 
 val invoke_pos = #pos o the_kind;
 val invoke_empty = #empty o the_kind;
 
 fun invoke_merge kind args =
   if ! data_timing then
     Timing.cond_timeit true ("Theory_Data.merge" ^ Position.here (#pos kind))
       (fn () => #merge kind args)
   else #merge kind args;
 
 fun declare_data pos empty merge =
   let
     val k = data_kind ();
     val kind = {pos = pos, empty = empty, merge = merge};
     val _ = Synchronized.change kinds (Datatab.update (k, kind));
   in k end;
 
 fun lookup_data k thy = Datatab.lookup (data_of thy) k;
 
 fun get_data k thy =
   (case lookup_data k thy of
     SOME x => x
   | NONE => invoke_empty k);
 
 fun merge_data [] = Datatab.empty
   | merge_data [thy] = data_of thy
   | merge_data thys =
       let
         fun merge (k, kind) data =
           (case map_filter (fn thy => lookup_data k thy |> Option.map (pair thy)) thys of
             [] => data
           | [(_, x)] => Datatab.default (k, x) data
           | args => Datatab.update (k, invoke_merge kind args) data);
       in Datatab.fold merge (Synchronized.value kinds) (data_of (hd thys)) end;
 
 end;
 
 
 
 (** build theories **)
 
 (* create theory *)
 
 fun create_thy state ids name stage ancestry data =
   let
     val theory_id = make_theory_id {id = new_id (), ids = ids, name = name, stage = stage};
     val (token, pos, assign) = theory_token ();
     val identity = {theory_id = theory_id, theory_token = token, theory_token_pos = pos};
   in assign (Thy (state, identity, ancestry, data)) end;
 
 
 (* primitives *)
 
 val pre_pure_thy =
   let
     val state = make_state ();
     val stage = next_stage state;
   in create_thy state Intset.empty PureN stage (make_ancestry [] []) Datatab.empty end;
 
 local
 
 fun change_thy finish f thy =
   let
     val {name, stage, ...} = identity_of thy;
     val Thy (state, _, ancestry, data) = thy;
     val ancestry' =
       if stage_final stage
       then make_ancestry [thy] (extend_ancestors thy (ancestors_of thy))
       else ancestry;
     val ids' = merge_ids [thy];
     val stage' = if finish then 0 else next_stage state;
     val data' = f data;
   in create_thy state ids' name stage' ancestry' data' end;
 
 in
 
 val update_thy = change_thy false;
 val finish_thy = change_thy true I;
 
 end;
 
 
 (* join: unfinished theory nodes *)
 
 fun join_thys [] = raise List.Empty
   | join_thys thys =
       let
         val thy0 = hd thys;
         val name0 = theory_long_name thy0;
         val state0 = state_of thy0;
 
         fun ok thy =
           not (theory_id_final (theory_id thy)) andalso
           theory_long_name thy = name0 andalso
           eq_ancestry (thy0, thy);
         val _ =
           (case filter_out ok thys of
             [] => ()
           | bad => raise THEORY ("Cannot join theories", bad));
 
         val stage = next_stage state0;
         val ids = merge_ids thys;
         val data = merge_data thys;
       in create_thy state0 ids name0 stage (ancestry_of thy0) data end;
 
 
 (* merge: finished theory nodes *)
 
 fun make_parents thys =
   let val thys' = distinct eq_thy thys
   in thys' |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys') end;
 
 fun begin_thy name imports =
   if name = "" then error ("Bad theory name: " ^ quote name)
   else if null imports then error "Missing theory imports"
   else
     let
       val parents = make_parents imports;
       val ancestors =
         Library.foldl1 merge_ancestors (map ancestors_of parents)
         |> fold extend_ancestors parents;
       val ancestry = make_ancestry parents ancestors;
 
       val state = make_state ();
       val stage = next_stage state;
       val ids = merge_ids parents;
       val data = merge_data parents;
     in create_thy state ids name stage ancestry data |> tap finish_thy end;
 
 
 (* theory data *)
 
 structure Theory_Data =
 struct
 
 val declare = declare_data;
 
 fun get k dest thy = dest (get_data k thy);
 
 fun put k make x = update_thy (Datatab.update (k, make x));
 
 fun sizeof1 k thy =
   Datatab.lookup (data_of thy) k |> Option.map ML_Heap.sizeof1;
 
 end;
 
 fun theory_data_sizeof1 thy =
   build (data_of thy |> Datatab.fold_rev (fn (k, _) =>
     (case Theory_Data.sizeof1 k thy of
       NONE => I
     | SOME n => (cons (invoke_pos k, n)))));
 
 
 
 (*** proof context ***)
 
 (* proof data kinds *)
 
 local
 
 val kinds = Synchronized.var "Proof_Data" (Datatab.empty: (theory -> Any.T) Datatab.table);
 
 fun init_data thy =
   Synchronized.value kinds |> Datatab.map (fn _ => fn init => init thy);
 
 fun init_new_data thy =
   Synchronized.value kinds |> Datatab.fold (fn (k, init) => fn data =>
     if Datatab.defined data k then data
     else Datatab.update (k, init thy) data);
 
 fun init_fallback k thy =
   (case Datatab.lookup (Synchronized.value kinds) k of
     SOME init => init thy
   | NONE => raise Fail "Invalid proof data identifier");
 
 in
 
 fun raw_transfer thy' (ctxt as Prf (_, _, thy, data)) =
   if eq_thy (thy, thy') then ctxt
   else if proper_subthy (thy, thy') then
     let
       val (token', pos', assign) = proof_token ();
       val data' = init_new_data thy' data;
     in assign (Prf (token', pos', thy', data')) end
   else error "Cannot transfer proof context: not a super theory";
 
 structure Proof_Context =
 struct
   fun theory_of (Prf (_, _, thy, _)) = thy;
   fun init_global thy =
     let val (token, pos, assign) = proof_token ()
     in assign (Prf (token, pos, thy, init_data thy)) end;
   fun get_global long thy name = init_global (get_theory long thy name);
 end;
 
 structure Proof_Data =
 struct
 
 fun declare init =
   let
     val k = data_kind ();
     val _ = Synchronized.change kinds (Datatab.update (k, init));
   in k end;
 
 fun get k dest (Prf (_, _, thy, data)) =
   (case Datatab.lookup data k of
     SOME x => x
   | NONE => init_fallback k thy) |> dest;
 
 fun put k make x (Prf (_, _, thy, data)) =
   let
     val (token', pos', assign) = proof_token ();
     val data' = Datatab.update (k, make x) data;
   in assign (Prf (token', pos', thy, data')) end;
 
 end;
 
 end;
 
 
 
 (*** theory certificate ***)
 
 datatype certificate = Certificate of theory | Certificate_Id of theory_id;
 
 fun certificate_theory (Certificate thy) = thy
   | certificate_theory (Certificate_Id thy_id) =
       error ("No content for theory certificate " ^ display_name thy_id);
 
 fun certificate_theory_id (Certificate thy) = theory_id thy
   | certificate_theory_id (Certificate_Id thy_id) = thy_id;
 
 fun eq_certificate (Certificate thy1, Certificate thy2) = eq_thy (thy1, thy2)
   | eq_certificate (Certificate_Id thy_id1, Certificate_Id thy_id2) = eq_thy_id (thy_id1, thy_id2)
   | eq_certificate _ = false;
 
 fun err_join (thy_id1, thy_id2) =
   error ("Cannot join unrelated theory certificates " ^
     display_name thy_id1 ^ " and " ^ display_name thy_id2);
 
 fun join_certificate (cert1, cert2) =
   let val (thy_id1, thy_id2) = apply2 certificate_theory_id (cert1, cert2) in
     if eq_thy_id (thy_id1, thy_id2) then (case cert1 of Certificate _ => cert1 | _ => cert2)
     else if proper_subthy_id (thy_id2, thy_id1) then cert1
     else if proper_subthy_id (thy_id1, thy_id2) then cert2
     else err_join (thy_id1, thy_id2)
   end;
 
 fun join_certificate_theory (thy1, thy2) =
   let val (thy_id1, thy_id2) = apply2 theory_id (thy1, thy2) in
     if subthy_id (thy_id2, thy_id1) then thy1
     else if proper_subthy_id (thy_id1, thy_id2) then thy2
     else err_join (thy_id1, thy_id2)
   end;
 
 
 (*** generic context ***)
 
 fun cases f _ (Theory thy) = f thy
   | cases _ g (Proof prf) = g prf;
 
 fun mapping f g = cases (Theory o f) (Proof o g);
 fun mapping_result f g = cases (apsnd Theory o f) (apsnd Proof o g);
 
 val the_theory = cases I (fn _ => error "Ill-typed context: theory expected");
 val the_proof = cases (fn _ => error "Ill-typed context: proof expected") I;
 
 fun map_theory f = Theory o f o the_theory;
 fun map_proof f = Proof o f o the_proof;
 
 fun map_theory_result f = apsnd Theory o f o the_theory;
 fun map_proof_result f = apsnd Proof o f o the_proof;
 
 fun theory_map f = the_theory o f o Theory;
 fun proof_map f = the_proof o f o Proof;
 
 val theory_of = cases I Proof_Context.theory_of;
 val proof_of = cases Proof_Context.init_global I;
 
 
 
 (** thread data **)
 
 local val generic_context_var = Thread_Data.var () : generic Thread_Data.var in
 
 fun get_generic_context () = Thread_Data.get generic_context_var;
 val put_generic_context = Thread_Data.put generic_context_var;
 fun setmp_generic_context opt_context = Thread_Data.setmp generic_context_var opt_context;
 
 fun the_generic_context () =
   (case get_generic_context () of
     SOME context => context
   | _ => error "Unknown context");
 
 val the_global_context = theory_of o the_generic_context;
 val the_local_context = proof_of o the_generic_context;
 
 end;
 
 fun >>> f =
   let
     val (res, context') = f (the_generic_context ());
     val _ = put_generic_context (SOME context');
   in res end;
 
 nonfix >>;
 fun >> f = >>> (fn context => ((), f context));
 
 val _ = put_generic_context (SOME (Theory pre_pure_thy));
 
 end;
 
 structure Basic_Context: BASIC_CONTEXT = Context;
 open Basic_Context;
 
 
 
 (*** type-safe interfaces for data declarations ***)
 
 (** theory data **)
 
 signature THEORY_DATA'_ARGS =
 sig
   type T
   val empty: T
   val merge: (theory * T) list -> T
 end;
 
 signature THEORY_DATA_ARGS =
 sig
   type T
   val empty: T
   val merge: T * T -> T
 end;
 
 signature THEORY_DATA =
 sig
   type T
   val get: theory -> T
   val put: T -> theory -> theory
   val map: (T -> T) -> theory -> theory
 end;
 
 functor Theory_Data'(Data: THEORY_DATA'_ARGS): THEORY_DATA =
 struct
 
 type T = Data.T;
 exception Data of T;
 
 val kind =
   let val pos = Position.thread_data () in
     Context.Theory_Data.declare
       pos
       (Data Data.empty)
       (Data o Data.merge o map (fn (thy, Data x) => (thy, x)))
   end;
 
 val get = Context.Theory_Data.get kind (fn Data x => x);
 val put = Context.Theory_Data.put kind Data;
 fun map f thy = put (f (get thy)) thy;
 
 end;
 
 functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
   Theory_Data'
   (
     type T = Data.T;
     val empty = Data.empty;
     fun merge args = Library.foldl (fn (a, (_, b)) => Data.merge (a, b)) (#2 (hd args), tl args)
   );
 
 
 
 (** proof data **)
 
 signature PROOF_DATA_ARGS =
 sig
   type T
   val init: theory -> T
 end;
 
 signature PROOF_DATA =
 sig
   type T
   val get: Proof.context -> T
   val put: T -> Proof.context -> Proof.context
   val map: (T -> T) -> Proof.context -> Proof.context
 end;
 
 functor Proof_Data(Data: PROOF_DATA_ARGS): PROOF_DATA =
 struct
 
 type T = Data.T;
 exception Data of T;
 
 val kind = Context.Proof_Data.declare (Data o Data.init);
 
 val get = Context.Proof_Data.get kind (fn Data x => x);
 val put = Context.Proof_Data.put kind Data;
 fun map f prf = put (f (get prf)) prf;
 
 end;
 
 
 
 (** generic data **)
 
 signature GENERIC_DATA_ARGS =
 sig
   type T
   val empty: T
   val merge: T * T -> T
 end;
 
 signature GENERIC_DATA =
 sig
   type T
   val get: Context.generic -> T
   val put: T -> Context.generic -> Context.generic
   val map: (T -> T) -> Context.generic -> Context.generic
 end;
 
 functor Generic_Data(Data: GENERIC_DATA_ARGS): GENERIC_DATA =
 struct
 
 structure Thy_Data = Theory_Data(Data);
 structure Prf_Data = Proof_Data(type T = Data.T val init = Thy_Data.get);
 
 type T = Data.T;
 
 fun get (Context.Theory thy) = Thy_Data.get thy
   | get (Context.Proof prf) = Prf_Data.get prf;
 
 fun put x (Context.Theory thy) = Context.Theory (Thy_Data.put x thy)
   | put x (Context.Proof prf) = Context.Proof (Prf_Data.put x prf);
 
 fun map f ctxt = put (f (get ctxt)) ctxt;
 
 end;
 
 (*hide private interface*)
 structure Context: CONTEXT = Context;
diff --git a/src/Pure/more_thm.ML b/src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML
+++ b/src/Pure/more_thm.ML
@@ -1,757 +1,757 @@
 (*  Title:      Pure/more_thm.ML
     Author:     Makarius
 
 Further operations on type ctyp/cterm/thm, outside the inference kernel.
 *)
 
 infix aconvc;
 
 signature BASIC_THM =
 sig
   include BASIC_THM
   val show_consts: bool Config.T
   val show_hyps: bool Config.T
   val show_tags: bool Config.T
   val aconvc: cterm * cterm -> bool
   type attribute = Context.generic * thm -> Context.generic option * thm option
 end;
 
 signature THM =
 sig
   include THM
   val eq_ctyp: ctyp * ctyp -> bool
   val aconvc: cterm * cterm -> bool
   val add_tvars: thm -> ctyp TVars.table -> ctyp TVars.table
   val add_vars: thm -> cterm Vars.table -> cterm Vars.table
   val dest_funT: ctyp -> ctyp * ctyp
   val strip_type: ctyp -> ctyp list * ctyp
   val instantiate_ctyp: ctyp TVars.table -> ctyp -> ctyp
   val all_name: Proof.context -> string * cterm -> cterm -> cterm
   val all: Proof.context -> cterm -> cterm -> cterm
   val mk_binop: cterm -> cterm -> cterm -> cterm
   val dest_binop: cterm -> cterm * cterm
   val dest_implies: cterm -> cterm * cterm
   val dest_equals: cterm -> cterm * cterm
   val dest_equals_lhs: cterm -> cterm
   val dest_equals_rhs: cterm -> cterm
   val lhs_of: thm -> cterm
   val rhs_of: thm -> cterm
   val is_reflexive: thm -> bool
   val eq_thm: thm * thm -> bool
   val eq_thm_prop: thm * thm -> bool
   val eq_thm_strict: thm * thm -> bool
   val equiv_thm: theory -> thm * thm -> bool
   val class_triv: theory -> class -> thm
   val of_sort: ctyp * sort -> thm list
   val is_dummy: thm -> bool
   val add_thm: thm -> thm list -> thm list
   val del_thm: thm -> thm list -> thm list
   val merge_thms: thm list * thm list -> thm list
   val item_net: thm Item_Net.T
   val item_net_intro: thm Item_Net.T
   val item_net_elim: thm Item_Net.T
   val declare_hyps: cterm -> Proof.context -> Proof.context
   val assume_hyps: cterm -> Proof.context -> thm * Proof.context
   val unchecked_hyps: Proof.context -> Proof.context
   val restore_hyps: Proof.context -> Proof.context -> Proof.context
   val undeclared_hyps: Context.generic -> thm -> term list
   val check_hyps: Context.generic -> thm -> thm
   val declare_term_sorts: term -> Proof.context -> Proof.context
   val extra_shyps': Proof.context -> thm -> sort list
   val check_shyps: Proof.context -> thm -> thm
   val weaken_sorts': Proof.context -> cterm -> cterm
   val elim_implies: thm -> thm -> thm
   val forall_intr_name: string * cterm -> thm -> thm
   val forall_elim_var: int -> thm -> thm
   val forall_elim_vars: int -> thm -> thm
   val instantiate_frees: ctyp TFrees.table * cterm Frees.table -> thm -> thm
   val instantiate': ctyp option list -> cterm option list -> thm -> thm
   val forall_intr_frees: thm -> thm
   val forall_intr_vars: thm -> thm
   val unvarify_global: theory -> thm -> thm
   val unvarify_axiom: theory -> string -> thm
   val rename_params_rule: string list * int -> thm -> thm
   val rename_boundvars: term -> term -> thm -> thm
   val add_axiom: Proof.context -> binding * term -> theory -> (string * thm) * theory
   val add_axiom_global: binding * term -> theory -> (string * thm) * theory
   val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory
   val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory
   type attribute = Context.generic * thm -> Context.generic option * thm option
   type binding = binding * attribute list
   val tag_rule: string * string -> thm -> thm
   val untag_rule: string -> thm -> thm
   val is_free_dummy: thm -> bool
   val tag_free_dummy: thm -> thm
   val def_name: string -> string
   val def_name_optional: string -> string -> string
   val def_binding: Binding.binding -> Binding.binding
   val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding
   val make_def_binding: bool -> Binding.binding -> Binding.binding
   val has_name_hint: thm -> bool
   val get_name_hint: thm -> string
   val put_name_hint: string -> thm -> thm
   val theoremK: string
   val legacy_get_kind: thm -> string
   val kind_rule: string -> thm -> thm
   val rule_attribute: thm list -> (Context.generic -> thm -> thm) -> attribute
   val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
   val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute
   val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic
   val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic
   val theory_attributes: attribute list -> thm -> theory -> thm * theory
   val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context
   val no_attributes: 'a -> 'a * 'b list
   val simple_fact: 'a -> ('a * 'b list) list
   val tag: string * string -> attribute
   val untag: string -> attribute
   val kind: string -> attribute
   val register_proofs: thm list lazy -> theory -> theory
   val consolidate_theory: theory -> unit
   val expose_theory: theory -> unit
   val show_consts: bool Config.T
   val show_hyps: bool Config.T
   val show_tags: bool Config.T
   val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T
   val pretty_thm: Proof.context -> thm -> Pretty.T
   val pretty_thm_item: Proof.context -> thm -> Pretty.T
   val pretty_thm_global: theory -> thm -> Pretty.T
   val string_of_thm: Proof.context -> thm -> string
   val string_of_thm_global: theory -> thm -> string
 end;
 
 structure Thm: THM =
 struct
 
 (** basic operations **)
 
 (* collecting ctyps and cterms *)
 
 val eq_ctyp = op = o apply2 Thm.typ_of;
 val op aconvc = op aconv o apply2 Thm.term_of;
 
 val add_tvars =
   Thm.fold_atomic_ctyps {hyps = false} Term.is_TVar (fn cT => fn tab =>
     let val v = Term.dest_TVar (Thm.typ_of cT)
     in tab |> not (TVars.defined tab v) ? TVars.add (v, cT) end);
 
 val add_vars =
   Thm.fold_atomic_cterms {hyps = false} Term.is_Var (fn ct => fn tab =>
     let val v = Term.dest_Var (Thm.term_of ct)
     in tab |> not (Vars.defined tab v) ? Vars.add (v, ct) end);
 
 
 (* ctyp operations *)
 
 fun dest_funT cT =
   (case Thm.typ_of cT of
     Type ("fun", _) => let val [A, B] = Thm.dest_ctyp cT in (A, B) end
   | T => raise TYPE ("dest_funT", [T], []));
 
 (* ctyp version of strip_type: maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T) *)
 fun strip_type cT =
   (case Thm.typ_of cT of
     Type ("fun", _) =>
       let
         val (cT1, cT2) = dest_funT cT;
         val (cTs, cT') = strip_type cT2
       in (cT1 :: cTs, cT') end
   | _ => ([], cT));
 
 fun instantiate_ctyp instT cT =
   Thm.instantiate_cterm (instT, Vars.empty) (Thm.var (("x", 0), cT))
   |> Thm.ctyp_of_cterm;
 
 
 (* cterm operations *)
 
 fun all_name ctxt (x, t) A =
   let
     val T = Thm.typ_of_cterm t;
     val all_const = Thm.cterm_of ctxt (Const ("Pure.all", (T --> propT) --> propT));
   in Thm.apply all_const (Thm.lambda_name (x, t) A) end;
 
 fun all ctxt t A = all_name ctxt ("", t) A;
 
 fun mk_binop c a b = Thm.apply (Thm.apply c a) b;
 fun dest_binop ct = (Thm.dest_arg1 ct, Thm.dest_arg ct);
 
 fun dest_implies ct =
   (case Thm.term_of ct of
     Const ("Pure.imp", _) $ _ $ _ => dest_binop ct
   | _ => raise TERM ("dest_implies", [Thm.term_of ct]));
 
 fun dest_equals ct =
   (case Thm.term_of ct of
     Const ("Pure.eq", _) $ _ $ _ => dest_binop ct
   | _ => raise TERM ("dest_equals", [Thm.term_of ct]));
 
 fun dest_equals_lhs ct =
   (case Thm.term_of ct of
     Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg1 ct
   | _ => raise TERM ("dest_equals_lhs", [Thm.term_of ct]));
 
 fun dest_equals_rhs ct =
   (case Thm.term_of ct of
     Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg ct
   | _ => raise TERM ("dest_equals_rhs", [Thm.term_of ct]));
 
 val lhs_of = dest_equals_lhs o Thm.cprop_of;
 val rhs_of = dest_equals_rhs o Thm.cprop_of;
 
 
 (* equality *)
 
 fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th))
   handle TERM _ => false;
 
 val eq_thm = is_equal o Thm.thm_ord;
 
 val eq_thm_prop = op aconv o apply2 Thm.full_prop_of;
 
 fun eq_thm_strict ths =
   eq_thm ths andalso
   Context.eq_thy_id (apply2 Thm.theory_id ths) andalso
   op = (apply2 Thm.maxidx_of ths) andalso
   op = (apply2 Thm.get_tags ths);
 
 
 (* pattern equivalence *)
 
 fun equiv_thm thy ths =
   Pattern.equiv thy (apply2 (Thm.full_prop_of o Thm.transfer thy) ths);
 
 
 (* type classes and sorts *)
 
 fun class_triv thy c =
   Thm.of_class (Thm.global_ctyp_of thy (TVar ((Name.aT, 0), [c])), c);
 
 fun of_sort (T, S) = map (fn c => Thm.of_class (T, c)) S;
 
 
 (* misc operations *)
 
 fun is_dummy thm =
   (case try Logic.dest_term (Thm.concl_of thm) of
     NONE => false
   | SOME t => Term.is_dummy_pattern (Term.head_of t));
 
 
 (* collections of theorems in canonical order *)
 
 val add_thm = update eq_thm_prop;
 val del_thm = remove eq_thm_prop;
 val merge_thms = merge eq_thm_prop;
 
 val item_net = Item_Net.init eq_thm_prop (single o Thm.full_prop_of);
 val item_net_intro = Item_Net.init eq_thm_prop (single o Thm.concl_of);
 val item_net_elim = Item_Net.init eq_thm_prop (single o Thm.major_prem_of);
 
 
 
 (** declared hyps and sort hyps **)
 
 structure Hyps = Proof_Data
 (
   type T = {checked_hyps: bool, hyps: Termset.T, shyps: sort Ord_List.T};
   fun init _ : T = {checked_hyps = true, hyps = Termset.empty, shyps = []};
 );
 
 fun map_hyps f = Hyps.map (fn {checked_hyps, hyps, shyps} =>
   let val (checked_hyps', hyps', shyps') = f (checked_hyps, hyps, shyps)
   in {checked_hyps = checked_hyps', hyps = hyps', shyps = shyps'} end);
 
 
 (* hyps *)
 
 fun declare_hyps raw_ct ctxt = ctxt |> map_hyps (fn (checked_hyps, hyps, shyps) =>
   let
     val ct = Thm.transfer_cterm' ctxt raw_ct;
     val hyps' = Termset.insert (Thm.term_of ct) hyps;
   in (checked_hyps, hyps', shyps) end);
 
 fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt);
 
 val unchecked_hyps = map_hyps (fn (_, hyps, shyps) => (false, hyps, shyps));
 
 fun restore_hyps ctxt =
   map_hyps (fn (_, hyps, shyps) => (#checked_hyps (Hyps.get ctxt), hyps, shyps));
 
 fun undeclared_hyps context th =
   Thm.hyps_of th
   |> filter_out
     (case context of
       Context.Theory _ => K false
     | Context.Proof ctxt =>
         (case Hyps.get ctxt of
           {checked_hyps = false, ...} => K true
         | {hyps, ...} => Termset.member hyps));
 
 fun check_hyps context th =
   (case undeclared_hyps context th of
     [] => th
   | undeclared =>
       error (Pretty.string_of (Pretty.big_list "Undeclared hyps:"
         (map (Pretty.item o single o Syntax.pretty_term (Syntax.init_pretty context)) undeclared))));
 
 
 (* shyps *)
 
 fun declare_term_sorts t =
   map_hyps (fn (checked_hyps, hyps, shyps) =>
     (checked_hyps, hyps, Sorts.insert_term t shyps));
 
 fun extra_shyps' ctxt th =
   Sorts.subtract (#shyps (Hyps.get ctxt)) (Thm.extra_shyps th);
 
 fun check_shyps ctxt raw_th =
   let
     val th = Thm.strip_shyps raw_th;
     val extra_shyps = extra_shyps' ctxt th;
   in
     if null extra_shyps then th
     else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" ::
       Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) extra_shyps))))
   end;
 
 val weaken_sorts' = Thm.weaken_sorts o #shyps o Hyps.get;
 
 
 
 (** basic derived rules **)
 
 (*Elimination of implication
   A    A \<Longrightarrow> B
   ------------
         B
 *)
 fun elim_implies thA thAB = Thm.implies_elim thAB thA;
 
 
 (* forall_intr_name *)
 
 fun forall_intr_name (a, x) th =
   let
     val th' = Thm.forall_intr x th;
     val prop' = (case Thm.prop_of th' of all $ Abs (_, T, b) => all $ Abs (a, T, b));
   in Thm.renamed_prop prop' th' end;
 
 
 (* forall_elim_var(s) *)
 
 local
 
 val used_frees =
   Name.build_context o
     Thm.fold_terms {hyps = true} Term.declare_term_frees;
 
 fun used_vars i =
   Name.build_context o
     (Thm.fold_terms {hyps = false} o Term.fold_aterms)
       (fn Var ((x, j), _) => i = j ? Name.declare x | _ => I);
 
 fun dest_all ct used =
   (case Thm.term_of ct of
     Const ("Pure.all", _) $ Abs (x, _, _) =>
       let
         val (x', used') = Name.variant x used;
         val (v, ct') = Thm.dest_abs_fresh x' (Thm.dest_arg ct);
       in SOME ((x, Thm.ctyp_of_cterm v), (ct', used')) end
   | _ => NONE);
 
 fun dest_all_list ct used =
   (case dest_all ct used of
     NONE => ([], used)
   | SOME (v, (ct', used')) =>
       let val (vs, used'') = dest_all_list ct' used'
       in (v :: vs, used'') end);
 
 fun forall_elim_vars_list vars i th =
   let
     val (vars', _) =
       (vars, used_vars i th) |-> fold_map (fn (x, T) => fn used =>
         let val (x', used') = Name.variant x used
         in (Thm.var ((x', i), T), used') end);
   in fold Thm.forall_elim vars' th end;
 
 in
 
 fun forall_elim_vars i th =
   forall_elim_vars_list (#1 (dest_all_list (Thm.cprop_of th) (used_frees th))) i th;
 
 fun forall_elim_var i th =
   let
     val vars =
       (case dest_all (Thm.cprop_of th) (used_frees th) of
         SOME (v, _) => [v]
       | NONE => raise THM ("forall_elim_var", i, [th]));
   in forall_elim_vars_list vars i th end;
 
 end;
 
 
 (* instantiate frees *)
 
 fun instantiate_frees (instT, inst) th =
   if TFrees.is_empty instT andalso Frees.is_empty inst then th
   else
     let
       val idx = Thm.maxidx_of th + 1;
       fun index ((a, A), b) = (((a, idx), A), b);
       val insts =
         (TVars.build (TFrees.fold (TVars.add o index) instT),
          Vars.build (Frees.fold (Vars.add o index) inst));
       val tfrees = Names.build (TFrees.fold (Names.add_set o #1 o #1) instT);
       val frees = Names.build (Frees.fold (Names.add_set o #1 o #1) inst);
 
       val hyps = Thm.chyps_of th;
       val inst_cterm =
         Thm.generalize_cterm (tfrees, frees) idx #>
         Thm.instantiate_cterm insts;
     in
       th
       |> fold_rev Thm.implies_intr hyps
       |> Thm.generalize (tfrees, frees) idx
       |> Thm.instantiate insts
       |> fold (elim_implies o Thm.assume o inst_cterm) hyps
     end;
 
 
 (* instantiate by left-to-right occurrence of variables *)
 
 fun instantiate' cTs cts thm =
   let
     fun err msg =
       raise TYPE ("instantiate': " ^ msg,
         map_filter (Option.map Thm.typ_of) cTs,
         map_filter (Option.map Thm.term_of) cts);
 
     fun zip_vars xs ys =
       zip_options xs ys handle ListPair.UnequalLengths =>
         err "more instantiations than variables in thm";
 
     val instT = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_tvars thm)) cTs;
     val thm' = Thm.instantiate (TVars.make instT, Vars.empty) thm;
     val inst = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_vars thm')) cts;
   in Thm.instantiate (TVars.empty, Vars.make inst) thm' end;
 
 
 (* implicit generalization over variables -- canonical order *)
 
 fun forall_intr_vars th =
   let val vars = Cterms.build (Cterms.add_vars th)
   in fold_rev Thm.forall_intr (Cterms.list_set vars) th end;
 
 fun forall_intr_frees th =
   let
     val fixed =
       Frees.build
        (fold Frees.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th)) #>
         fold Frees.add_frees (Thm.hyps_of th));
     val is_fixed = Frees.defined fixed o Term.dest_Free o Thm.term_of;
     val frees =
       Cterms.build (th |> Thm.fold_atomic_cterms {hyps = false} Term.is_Free
         (fn ct => not (is_fixed ct) ? Cterms.add_set ct));
   in fold_rev Thm.forall_intr (Cterms.list_set frees) th end;
 
 
 (* unvarify_global: global schematic variables *)
 
 fun unvarify_global thy th =
   let
     val prop = Thm.full_prop_of th;
     val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th)
       handle TERM (msg, _) => raise THM (msg, 0, [th]);
 
     val cert = Thm.global_cterm_of thy;
     val certT = Thm.global_ctyp_of thy;
 
     val instT =
       TVars.build (prop |> (Term.fold_types o Term.fold_atyps)
         (fn T => fn instT =>
           (case T of
             TVar (v as ((a, _), S)) =>
               if TVars.defined instT v then instT
               else TVars.add (v, TFree (a, S)) instT
           | _ => instT)));
     val cinstT = TVars.map (K certT) instT;
     val cinst =
       Vars.build (prop |> Term.fold_aterms
         (fn t => fn inst =>
           (case t of
             Var ((x, i), T) =>
               let val T' = Term_Subst.instantiateT instT T
               in Vars.add (((x, i), T'), cert (Free ((x, T')))) inst end
           | _ => inst)));
   in Thm.instantiate (cinstT, cinst) th end;
 
 fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy;
 
 
 (* user renaming of parameters in a subgoal *)
 
 (*The names, if distinct, are used for the innermost parameters of subgoal i;
   preceding parameters may be renamed to make all parameters distinct.*)
 fun rename_params_rule (names, i) st =
   let
     val (_, Bs, Bi, C) = Thm.dest_state (st, i);
     val params = map #1 (Logic.strip_params Bi);
     val short = length params - length names;
     val names' =
       if short < 0 then error "More names than parameters in subgoal!"
       else Name.variant_list names (take short params) @ names;
     val free_names = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi [];
     val Bi' = Logic.list_rename_params names' Bi;
   in
     (case duplicates (op =) names of
       a :: _ => (warning ("Can't rename.  Bound variables not distinct: " ^ a); st)
     | [] =>
       (case inter (op =) names free_names of
         a :: _ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); st)
       | [] => Thm.renamed_prop (Logic.list_implies (Bs @ [Bi'], C)) st))
   end;
 
 
 (* preservation of bound variable names *)
 
 fun rename_boundvars pat obj th =
   (case Term.rename_abs pat obj (Thm.prop_of th) of
     NONE => th
   | SOME prop' => Thm.renamed_prop prop' th);
 
 
 
 (** specification primitives **)
 
 (* rules *)
 
 fun stripped_sorts thy t =
   let
     val tfrees = build_rev (Term.add_tfrees t);
     val tfrees' = map (fn a => (a, [])) (Name.variant_list [] (map #1 tfrees));
     val recover =
       map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S))))
         tfrees' tfrees;
     val strip = map (apply2 TFree) (tfrees ~~ tfrees');
     val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t;
   in (strip, recover, t') end;
 
 fun add_axiom ctxt (b, prop) thy =
   let
     val _ = Sign.no_vars ctxt prop;
     val (strip, recover, prop') = stripped_sorts thy prop;
     val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
     val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of ctxt T, S)) strip;
 
     val thy' = thy
       |> Theory.add_axiom ctxt (b, Logic.list_implies (maps Logic.mk_of_sort constraints, prop'));
     val axm_name = Sign.full_name thy' b;
     val axm' = Thm.axiom thy' axm_name;
     val thm =
       Thm.instantiate (TVars.make recover, Vars.empty) axm'
       |> unvarify_global thy'
       |> fold elim_implies of_sorts;
   in ((axm_name, thm), thy') end;
 
 fun add_axiom_global arg thy = add_axiom (Syntax.init_pretty_global thy) arg thy;
 
 fun add_def (context as (ctxt, _)) unchecked overloaded (b, prop) thy =
   let
     val _ = Sign.no_vars ctxt prop;
     val prems = map (Thm.cterm_of ctxt) (Logic.strip_imp_prems prop);
     val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
 
     val thy' = Theory.add_def context unchecked overloaded (b, concl') thy;
     val axm_name = Sign.full_name thy' b;
     val axm' = Thm.axiom thy' axm_name;
     val thm =
       Thm.instantiate (TVars.make recover, Vars.empty) axm'
       |> unvarify_global thy'
       |> fold_rev Thm.implies_intr prems;
   in ((axm_name, thm), thy') end;
 
 fun add_def_global unchecked overloaded arg thy =
   add_def (Defs.global_context thy) unchecked overloaded arg thy;
 
 
 
 (** theorem tags **)
 
 (* add / delete tags *)
 
 fun tag_rule tg = Thm.map_tags (insert (op =) tg);
 fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s'));
 
 
 (* free dummy thm -- for abstract closure *)
 
 val free_dummyN = "free_dummy";
 fun is_free_dummy thm = Properties.defined (Thm.get_tags thm) free_dummyN;
 val tag_free_dummy = tag_rule (free_dummyN, "");
 
 
 (* def_name *)
 
 fun def_name c = c ^ "_def";
 
 fun def_name_optional c "" = def_name c
   | def_name_optional _ name = name;
 
 val def_binding = Binding.map_name def_name #> Binding.reset_pos;
 fun def_binding_optional b name = if Binding.is_empty name then def_binding b else name;
 fun make_def_binding cond b = if cond then def_binding b else Binding.empty;
 
 
 (* unofficial theorem names *)
 
 fun has_name_hint thm = AList.defined (op =) (Thm.get_tags thm) Markup.nameN;
 fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN);
 fun get_name_hint thm = if has_name_hint thm then the_name_hint thm else "??.unknown";
 
 fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name);
 
 
 (* theorem kinds *)
 
 val theoremK = "theorem";
 
-fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN);
+fun legacy_get_kind thm = Properties.get_string (Thm.get_tags thm) Markup.kindN;
 
 fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN;
 
 
 
 (** attributes **)
 
 (*attributes subsume any kind of rules or context modifiers*)
 type attribute = Context.generic * thm -> Context.generic option * thm option;
 
 type binding = binding * attribute list;
 
 fun rule_attribute ths f (x, th) =
   (NONE,
     (case find_first is_free_dummy (th :: ths) of
       SOME th' => SOME th'
     | NONE => SOME (f x th)));
 
 fun declaration_attribute f (x, th) =
   (if is_free_dummy th then NONE else SOME (f th x), NONE);
 
 fun mixed_attribute f (x, th) =
   let val (x', th') = f (x, th) in (SOME x', SOME th') end;
 
 fun apply_attribute (att: attribute) th x =
   let val (x', th') = att (x, check_hyps x (Thm.transfer'' x th))
   in (the_default th th', the_default x x') end;
 
 fun attribute_declaration att th x = #2 (apply_attribute att th x);
 
 fun apply_attributes mk dest =
   let
     fun app [] th x = (th, x)
       | app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts;
   in app end;
 
 val theory_attributes = apply_attributes Context.Theory Context.the_theory;
 val proof_attributes = apply_attributes Context.Proof Context.the_proof;
 
 fun no_attributes x = (x, []);
 fun simple_fact x = [(x, [])];
 
 fun tag tg = rule_attribute [] (K (tag_rule tg));
 fun untag s = rule_attribute [] (K (untag_rule s));
 fun kind k = rule_attribute [] (K (k <> "" ? kind_rule k));
 
 
 
 (** forked proofs **)
 
 structure Proofs = Theory_Data
 (
   type T = thm list lazy Inttab.table;
   val empty = Inttab.empty;
   val merge = Inttab.merge (K true);
 );
 
 fun reset_proofs thy =
   if Inttab.is_empty (Proofs.get thy) then NONE
   else SOME (Proofs.put Inttab.empty thy);
 
 val _ = Theory.setup (Theory.at_begin reset_proofs);
 
 fun register_proofs ths thy =
   let val entry = (serial (), Lazy.map_finished (map Thm.trim_context) ths)
   in (Proofs.map o Inttab.update) entry thy end;
 
 fun force_proofs thy =
   Proofs.get thy |> Inttab.dest |> maps (map (Thm.transfer thy) o Lazy.force o #2);
 
 val consolidate_theory = Thm.consolidate o force_proofs;
 
 fun expose_theory thy =
   if Proofterm.export_enabled ()
   then Thm.expose_proofs thy (force_proofs thy) else ();
 
 
 
 (** print theorems **)
 
 (* options *)
 
 val show_consts = Config.declare_option_bool ("show_consts", \<^here>);
 val show_hyps = Config.declare_bool ("show_hyps", \<^here>) (K false);
 val show_tags = Config.declare_bool ("show_tags", \<^here>) (K false);
 
 
 (* pretty_thm etc. *)
 
 fun pretty_tag (name, arg) = Pretty.strs [name, quote arg];
 val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
 
 fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th =
   let
     val show_tags = Config.get ctxt show_tags;
     val show_hyps = Config.get ctxt show_hyps;
 
     val th = raw_th
       |> perhaps (try (Thm.transfer' ctxt))
       |> perhaps (try Thm.strip_shyps);
 
     val hyps = if show_hyps then Thm.hyps_of th else undeclared_hyps (Context.Proof ctxt) th;
     val extra_shyps = extra_shyps' ctxt th;
     val tags = Thm.get_tags th;
     val tpairs = Thm.tpairs_of th;
 
     val q = if quote then Pretty.quote else I;
     val prt_term = q o Syntax.pretty_term ctxt;
 
 
     val hlen = length extra_shyps + length hyps + length tpairs;
     val hsymbs =
       if hlen = 0 then []
       else if show_hyps orelse show_hyps' then
         [Pretty.brk 2, Pretty.list "[" "]"
           (map (q o Pretty.block o Syntax.pretty_flexpair ctxt) tpairs @ map prt_term hyps @
            map (Syntax.pretty_sort ctxt) extra_shyps)]
       else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")];
     val tsymbs =
       if null tags orelse not show_tags then []
       else [Pretty.brk 1, pretty_tags tags];
   in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end;
 
 fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true};
 fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th];
 
 fun pretty_thm_global thy =
   pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false};
 
 val string_of_thm = Pretty.string_of oo pretty_thm;
 val string_of_thm_global = Pretty.string_of oo pretty_thm_global;
 
 
 open Thm;
 
 end;
 
 structure Basic_Thm: BASIC_THM = Thm;
 open Basic_Thm;