diff --git a/src/Pure/Isar/local_theory.ML b/src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML
+++ b/src/Pure/Isar/local_theory.ML
@@ -1,439 +1,440 @@
 (*  Title:      Pure/Isar/local_theory.ML
     Author:     Makarius
 
 Local theory operations, with abstract target context.
 *)
 
 type local_theory = Proof.context;
 type generic_theory = Context.generic;
 
 structure Attrib =
 struct
   type binding = binding * Token.src list;
   type thms = (thm list * Token.src list) list;
   type fact = binding * thms;
 end;
 
 structure Locale =
 struct
   type registration = {inst: string * morphism, mixin: (morphism * bool) option, export: morphism};
 end;
 
 signature LOCAL_THEORY =
 sig
   type operations
   val assert: local_theory -> local_theory
   val level: Proof.context -> int
   val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
   val background_naming_of: local_theory -> Name_Space.naming
   val map_background_naming: (Name_Space.naming -> Name_Space.naming) ->
     local_theory -> local_theory
   val restore_background_naming: local_theory -> local_theory -> local_theory
   val full_name: local_theory -> binding -> string
   val new_group: local_theory -> local_theory
   val reset_group: local_theory -> local_theory
   val standard_morphism: local_theory -> Proof.context -> morphism
   val standard_morphism_theory: local_theory -> morphism
   val standard_form: local_theory -> Proof.context -> 'a Morphism.entity -> 'a
   val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val raw_theory: (theory -> theory) -> local_theory -> local_theory
   val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val background_theory: (theory -> theory) -> local_theory -> local_theory
   val target_of: local_theory -> Proof.context
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val target_morphism: local_theory -> morphism
   val propagate_ml_env: generic_theory -> generic_theory
   val touch_ml_env: generic_theory -> generic_theory
   val operations_of: local_theory -> operations
   val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
   val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
   val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
   val notes: Attrib.fact list -> local_theory -> (string * thm list) list * local_theory
   val notes_kind: string -> Attrib.fact list -> local_theory ->
     (string * thm list) list * local_theory
   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
   val declaration: {syntax: bool, pervasive: bool} -> Morphism.declaration_fn ->
     local_theory -> local_theory
   val theory_registration: Locale.registration -> local_theory -> local_theory
   val locale_dependency: Locale.registration -> local_theory -> local_theory
   val pretty: local_theory -> Pretty.T list
   val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory
   val set_defsort: sort -> local_theory -> local_theory
   val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list ->
     local_theory -> local_theory
   val syntax_cmd: bool -> Syntax.mode -> (string * string * mixfix) list ->
     local_theory -> local_theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
   val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list ->
     local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
   val type_alias: binding -> string -> local_theory -> local_theory
   val const_alias: binding -> string -> local_theory -> local_theory
   val init: {background_naming: Name_Space.naming, setup: theory -> Proof.context,
     conclude: local_theory -> Proof.context} -> operations -> theory -> local_theory
   val exit: local_theory -> Proof.context
   val exit_global: local_theory -> theory
   val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
   val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
   val begin_nested: local_theory -> Binding.scope * local_theory
   val end_nested: local_theory -> local_theory
   val end_nested_result: (morphism -> 'a -> 'b) ->  'a * local_theory -> 'b * local_theory
 end;
 
 signature PRIVATE_LOCAL_THEORY =
 sig
   include LOCAL_THEORY
   val reset: local_theory -> local_theory
 end
 
 structure Local_Theory: PRIVATE_LOCAL_THEORY =
 struct
 
 (** local theory data **)
 
 (* type lthy *)
 
 type operations =
  {define: bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory,
   notes: string -> Attrib.fact list -> local_theory -> (string * thm list) list * local_theory,
   abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory,
   declaration: {syntax: bool, pervasive: bool} -> Morphism.declaration ->
     local_theory -> local_theory,
   theory_registration: Locale.registration -> local_theory -> local_theory,
   locale_dependency: Locale.registration -> local_theory -> local_theory,
   pretty: local_theory -> Pretty.T list};
 
 type lthy =
  {background_naming: Name_Space.naming,
   operations: operations,
   conclude: Proof.context -> Proof.context,
   target: Proof.context};
 
 fun make_lthy (background_naming, operations, conclude, target) : lthy =
   {background_naming = background_naming, operations = operations,
     conclude = conclude, target = target};
 
 
 (* context data *)
 
 structure Data = Proof_Data
 (
   type T = lthy list;
   fun init _ = [];
 );
 
 
 (* nested structure *)
 
 val level = length o Data.get;  (*1: main target at bottom, >= 2: nested target context*)
 
 fun assert lthy =
   if level lthy = 0 then error "Missing local theory context" else lthy;
 
 fun assert_bottom lthy =
   let
     val _ = assert lthy;
   in
     if level lthy > 1 then error "Not at bottom of local theory nesting"
     else lthy
   end;
 
 fun assert_not_bottom lthy =
   let
     val _ = assert lthy;
   in
     if level lthy = 1 then error "Already at bottom of local theory nesting"
     else lthy
   end;
 
 val bottom_of = List.last o Data.get o assert;
 val top_of = hd o Data.get o assert;
 
 fun map_top f =
   assert #>
   Data.map (fn {background_naming, operations, conclude, target} :: parents =>
     make_lthy (f (background_naming, operations, conclude, target)) :: parents);
 
 fun reset lthy = #target (top_of lthy) |> Data.put (Data.get lthy);
 
 fun map_contexts f lthy =
   let val n = level lthy in
     lthy |> (Data.map o map_index)
       (fn (i, {background_naming, operations, conclude, target}) =>
         make_lthy (background_naming, operations, conclude,
           target
           |> Context_Position.set_visible false
           |> f (n - i - 1)
           |> Context_Position.restore_visible target))
       |> f n
   end;
 
 
 (* naming for background theory *)
 
 val background_naming_of = #background_naming o top_of;
 
 fun map_background_naming f =
   map_top (fn (background_naming, operations, conclude, target) =>
     (f background_naming, operations, conclude, target));
 
 val restore_background_naming = map_background_naming o K o background_naming_of;
 
 val full_name = Name_Space.full_name o background_naming_of;
 
 val new_group = map_background_naming Name_Space.new_group;
 val reset_group = map_background_naming Name_Space.reset_group;
 
 
 (* standard morphisms *)
 
 fun standard_morphism lthy ctxt =
   Morphism.set_context' lthy
-   (Proof_Context.norm_export_morphism lthy ctxt $>
+   (Proof_Context.export_morphism lthy ctxt $>
+    Morphism.thm_morphism' "Local_Theory.standard" (Goal.norm_result o Proof_Context.init_global) $>
     Morphism.binding_morphism "Local_Theory.standard_binding"
       (Name_Space.transform_binding (Proof_Context.naming_of lthy)));
 
 fun standard_morphism_theory lthy =
   standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
 
 fun standard_form lthy ctxt x =
   Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
 
 
 (* background theory *)
 
 fun raw_theory_result f lthy =
   let
     val (res, thy') = f (Proof_Context.theory_of lthy);
     val lthy' = map_contexts (K (Proof_Context.transfer thy')) lthy;
   in (res, lthy') end;
 
 fun raw_theory f = #2 o raw_theory_result (f #> pair ());
 
 fun background_theory_result f lthy =
   let
     val naming =
       background_naming_of lthy
       |> Name_Space.transform_naming (Proof_Context.naming_of lthy);
   in
     lthy |> raw_theory_result (fn thy =>
       thy
       |> Sign.map_naming (K naming)
       |> f
       ||> Sign.restore_naming thy)
   end;
 
 fun background_theory f = #2 o background_theory_result (f #> pair ());
 
 
 (* target contexts *)
 
 val target_of = #target o bottom_of;
 
 fun target f lthy =
   let
     val ctxt = target_of lthy;
     val ctxt' = ctxt
       |> Context_Position.set_visible false
       |> f
       |> Context_Position.restore_visible ctxt;
     val thy' = Proof_Context.theory_of ctxt';
   in map_contexts (fn 0 => K ctxt' | _ => Proof_Context.transfer thy') lthy end;
 
 fun target_morphism lthy = standard_morphism lthy (target_of lthy);
 
 fun propagate_ml_env (context as Context.Proof lthy) =
       let val inherit = ML_Env.inherit [context] in
         lthy
         |> background_theory (Context.theory_map inherit)
         |> map_contexts (K (Context.proof_map inherit))
         |> Context.Proof
       end
   | propagate_ml_env context = context;
 
 fun touch_ml_env context =
   if Context.enabled_tracing () then
     (case context of
       Context.Theory _ => ML_Env.touch context
     | Context.Proof _ => context)
   else context;
 
 
 
 (** operations **)
 
 val operations_of = #operations o top_of;
 
 fun operation f lthy = f (operations_of lthy) lthy;
 fun operation1 f x = operation (fn ops => f ops x);
 fun operation2 f x y = operation (fn ops => f ops x y);
 
 
 (* primitives *)
 
 val pretty = operation #pretty;
 val abbrev = operation2 #abbrev;
 val define = operation2 #define false;
 val define_internal = operation2 #define true;
 val notes_kind = operation2 #notes;
 fun declaration args = operation2 #declaration args o Morphism.entity;
 val theory_registration = operation1 #theory_registration;
 fun locale_dependency registration =
   assert_bottom #> operation1 #locale_dependency registration;
 
 
 (* theorems *)
 
 val notes = notes_kind "";
 fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
 
 fun add_thms_dynamic (binding, f) lthy =
   lthy
   |> background_theory_result (fn thy => thy
       |> Global_Theory.add_thms_dynamic' (Sign.inherit_naming thy lthy) (binding, f))
   |-> (fn name =>
     map_contexts (fn _ => fn ctxt =>
       Proof_Context.transfer_facts (Proof_Context.theory_of ctxt) ctxt) #>
     declaration {syntax = false, pervasive = false} (fn phi =>
       let val binding' = Morphism.binding phi binding in
         Context.mapping
           (Global_Theory.alias_fact binding' name)
           (Proof_Context.alias_fact binding' name)
       end));
 
 
 (* default sort *)
 
 fun set_defsort S =
   declaration {syntax = true, pervasive = false}
     (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
 
 
 (* syntax *)
 
 fun gen_syntax prep_type add mode raw_args lthy =
   let
     val args = map (fn (c, T, mx) => (c, prep_type lthy T, mx)) raw_args;
     val args' = map (fn (c, T, mx) => (c, T, Mixfix.reset_pos mx)) args;
     val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.syntax add mode args;
   in
     declaration {syntax = true, pervasive = false}
       (fn _ => Proof_Context.generic_syntax add mode args') lthy
   end;
 
 val syntax = gen_syntax (K I);
 val syntax_cmd = gen_syntax Proof_Context.read_typ_syntax;
 
 
 (* notation *)
 
 local
 
 fun gen_type_notation prep_type add mode raw_args lthy =
   let
     val prepare = prep_type lthy #> Logic.type_map (Assumption.export_term lthy (target_of lthy));
     val args = map (apfst prepare) raw_args;
     val args' = map (apsnd Mixfix.reset_pos) args;
     val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.type_notation add mode args;
   in
     declaration {syntax = true, pervasive = false}
       (Proof_Context.generic_type_notation add mode args') lthy
   end;
 
 fun gen_notation prep_const add mode raw_args lthy =
   let
     val prepare = prep_const lthy #> Assumption.export_term lthy (target_of lthy);
     val args = map (apfst prepare) raw_args;
     val args' = map (apsnd Mixfix.reset_pos) args;
     val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.notation add mode args;
   in
     declaration {syntax = true, pervasive = false}
       (Proof_Context.generic_notation add mode args') lthy
   end;
 
 in
 
 val type_notation = gen_type_notation (K I);
 val type_notation_cmd =
   gen_type_notation (Proof_Context.read_type_name {proper = true, strict = false});
 
 val notation = gen_notation (K I);
 val notation_cmd = gen_notation (Proof_Context.read_const {proper = false, strict = false});
 
 end;
 
 
 (* name space aliases *)
 
 fun syntax_alias global_alias local_alias b name =
   declaration {syntax = true, pervasive = false} (fn phi =>
     let val b' = Morphism.binding phi b
     in Context.mapping (global_alias b' name) (local_alias b' name) end);
 
 val type_alias = syntax_alias Sign.type_alias Proof_Context.type_alias;
 val const_alias = syntax_alias Sign.const_alias Proof_Context.const_alias;
 
 
 
 (** manage targets **)
 
 (* main target *)
 
 fun init_target background_naming conclude operations target =
   Data.map (K [make_lthy (background_naming, operations, conclude, target)]) target
 
 fun init {background_naming, setup, conclude} operations thy =
   thy
   |> Sign.change_begin
   |> setup
   |> init_target background_naming (conclude #> target_of #> Sign.change_end_local) operations;
 
 val exit_of = #conclude o bottom_of;
 
 fun exit lthy = exit_of lthy (assert_bottom lthy);
 val exit_global = Proof_Context.theory_of o exit;
 
 fun exit_result decl (x, lthy) =
   let
     val ctxt = exit lthy;
     val phi = standard_morphism lthy ctxt;
   in (decl phi x, ctxt) end;
 
 fun exit_result_global decl (x, lthy) =
   let
     val thy = exit_global lthy;
     val thy_ctxt = Proof_Context.init_global thy;
     val phi = standard_morphism lthy thy_ctxt;
   in (decl phi x, thy) end;
 
 
 (* nested targets *)
 
 fun begin_nested lthy =
   let
     val _ = assert lthy;
     val (scope, target) = Proof_Context.new_scope lthy;
     val entry = make_lthy (background_naming_of lthy, operations_of lthy,
       Proof_Context.restore_naming lthy, target);
     val lthy' = Data.map (cons entry) target;
   in (scope, lthy') end;
 
 fun end_nested lthy =
   let
     val _ = assert_not_bottom lthy;
     val ({conclude, ...} :: rest) = Data.get lthy;
   in lthy |> Data.put rest |> reset |> conclude end;
 
 fun end_nested_result decl (x, lthy) =
    let
     val outer_lthy = end_nested lthy;
     val phi = Proof_Context.export_morphism lthy outer_lthy;
   in (decl phi x, outer_lthy) end;
 
 end;
diff --git a/src/Pure/Isar/proof_context.ML b/src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML
+++ b/src/Pure/Isar/proof_context.ML
@@ -1,1676 +1,1671 @@
 (*  Title:      Pure/Isar/proof_context.ML
     Author:     Markus Wenzel, TU Muenchen
 
 The key concept of Isar proof contexts: elevates primitive local
 reasoning Gamma |- phi to a structured concept, with generic context
 elements.  See also structure Variable and Assumption.
 *)
 
 signature PROOF_CONTEXT =
 sig
   val theory_of: Proof.context -> theory
   val init_global: theory -> Proof.context
   val get_global: {long: bool} -> theory -> string -> Proof.context
   type mode
   val mode_default: mode
   val mode_pattern: mode
   val mode_schematic: mode
   val mode_abbrev: mode
   val set_mode: mode -> Proof.context -> Proof.context
   val get_mode: Proof.context -> mode
   val restore_mode: Proof.context -> Proof.context -> Proof.context
   val abbrev_mode: Proof.context -> bool
   val syn_of: Proof.context -> Syntax.syntax
   val tsig_of: Proof.context -> Type.tsig
   val set_defsort: sort -> Proof.context -> Proof.context
   val default_sort: Proof.context -> indexname -> sort
   val arity_sorts: Proof.context -> string -> sort -> sort list
   val consts_of: Proof.context -> Consts.T
   val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
   val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
   val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
   val naming_of: Proof.context -> Name_Space.naming
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val full_name: Proof.context -> binding -> string
   val get_scope: Proof.context -> Binding.scope option
   val new_scope: Proof.context -> Binding.scope * Proof.context
   val private_scope: Binding.scope -> Proof.context -> Proof.context
   val private: Position.T -> Proof.context -> Proof.context
   val qualified_scope: Binding.scope -> Proof.context -> Proof.context
   val qualified: Position.T -> Proof.context -> Proof.context
   val concealed: Proof.context -> Proof.context
   val class_space: Proof.context -> Name_Space.T
   val type_space: Proof.context -> Name_Space.T
   val const_space: Proof.context -> Name_Space.T
   val defs_context: Proof.context -> Defs.context
   val intern_class: Proof.context -> xstring -> string
   val intern_type: Proof.context -> xstring -> string
   val intern_const: Proof.context -> xstring -> string
   val extern_class: Proof.context -> string -> xstring
   val markup_class: Proof.context -> string -> string
   val pretty_class: Proof.context -> string -> Pretty.T
   val extern_type: Proof.context -> string -> xstring
   val markup_type: Proof.context -> string -> string
   val pretty_type: Proof.context -> string -> Pretty.T
   val extern_const: Proof.context -> string -> xstring
   val markup_const: Proof.context -> string -> string
   val pretty_const: Proof.context -> string -> Pretty.T
   val transfer: theory -> Proof.context -> Proof.context
   val transfer_facts: theory -> Proof.context -> Proof.context
   val background_theory: (theory -> theory) -> Proof.context -> Proof.context
   val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
   val facts_of: Proof.context -> Facts.T
   val facts_of_fact: Proof.context -> string -> Facts.T
   val markup_extern_fact: Proof.context -> string -> Markup.T list * xstring
   val augment: term -> Proof.context -> Proof.context
   val print_name: Proof.context -> string -> string
   val pretty_name: Proof.context -> string -> Pretty.T
   val pretty_term_abbrev: Proof.context -> term -> Pretty.T
   val pretty_fact: Proof.context -> string * thm list -> Pretty.T
   val check_class: Proof.context -> xstring * Position.T -> class * Position.report list
   val read_class: Proof.context -> string -> class
   val read_typ: Proof.context -> string -> typ
   val read_typ_syntax: Proof.context -> string -> typ
   val read_typ_abbrev: Proof.context -> string -> typ
   val cert_typ: Proof.context -> typ -> typ
   val cert_typ_syntax: Proof.context -> typ -> typ
   val cert_typ_abbrev: Proof.context -> typ -> typ
   val infer_type: Proof.context -> string * typ -> typ
   val inferred_param: string -> Proof.context -> (string * typ) * Proof.context
   val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
   val check_type_name: {proper: bool, strict: bool} -> Proof.context ->
     xstring * Position.T -> typ * Position.report list
   val read_type_name: {proper: bool, strict: bool} -> Proof.context -> string -> typ
   val consts_completion_message: Proof.context -> xstring * Position.T list -> string
   val check_const: {proper: bool, strict: bool} -> Proof.context ->
     xstring * Position.T list -> term * Position.report list
   val read_const: {proper: bool, strict: bool} -> Proof.context -> string -> term
   val read_arity: Proof.context -> xstring * string list * string -> arity
   val cert_arity: Proof.context -> arity -> arity
   val allow_dummies: Proof.context -> Proof.context
   val prepare_sortsT: Proof.context -> typ list -> string list * typ list
   val prepare_sorts: Proof.context -> term list -> string list * term list
   val check_tfree: Proof.context -> string * sort -> string * sort
   val read_term_pattern: Proof.context -> string -> term
   val read_term_schematic: Proof.context -> string -> term
   val read_term_abbrev: Proof.context -> string -> term
   val show_abbrevs: bool Config.T
   val expand_abbrevs: Proof.context -> term -> term
   val cert_term: Proof.context -> term -> term
   val cert_prop: Proof.context -> term -> term
   val def_type: Proof.context -> indexname -> typ option
   val standard_typ_check: Proof.context -> typ list -> typ list
   val standard_term_check_finish: Proof.context -> term list -> term list
   val standard_term_uncheck: Proof.context -> term list -> term list
   val goal_export: Proof.context -> Proof.context -> thm list -> thm list
   val export: Proof.context -> Proof.context -> thm list -> thm list
   val export_morphism: Proof.context -> Proof.context -> morphism
-  val norm_export_morphism: Proof.context -> Proof.context -> morphism
   val auto_bind_goal: term list -> Proof.context -> Proof.context
   val auto_bind_facts: term list -> Proof.context -> Proof.context
   val simult_matches: Proof.context -> term * term list -> (indexname * term) list
   val maybe_bind_term: indexname * term option -> Proof.context -> Proof.context
   val bind_term: indexname * term -> Proof.context -> Proof.context
   val cert_propp: Proof.context -> (term * term list) list list ->
     (term list list * (indexname * term) list)
   val read_propp: Proof.context -> (string * string list) list list ->
     (term list list * (indexname * term) list)
   val fact_tac: Proof.context -> thm list -> int -> tactic
   val some_fact_tac: Proof.context -> int -> tactic
   val lookup_fact: Proof.context -> string -> {dynamic: bool, thms: thm list} option
   val dynamic_facts_dummy: bool Config.T
   val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list
   val get_fact: Proof.context -> Facts.ref -> thm list
   val get_fact_single: Proof.context -> Facts.ref -> thm
   val get_thms: Proof.context -> xstring -> thm list
   val get_thm: Proof.context -> xstring -> thm
   val is_stmt: Proof.context -> bool
   val set_stmt: bool -> Proof.context -> Proof.context
   val restore_stmt: Proof.context -> Proof.context -> Proof.context
   val add_thms_dynamic: binding * (Context.generic -> thm list) ->
     Proof.context -> string * Proof.context
   val add_thms_lazy: string -> (binding * thm list lazy) -> Proof.context -> Proof.context
   val note_thms: string -> Thm.binding * (thm list * attribute list) list ->
     Proof.context -> (string * thm list) * Proof.context
   val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
   val alias_fact: binding -> string -> Proof.context -> Proof.context
   val read_var: binding * string option * mixfix -> Proof.context ->
     (binding * typ option * mixfix) * Proof.context
   val cert_var: binding * typ option * mixfix -> Proof.context ->
     (binding * typ option * mixfix) * Proof.context
   val add_fixes: (binding * typ option * mixfix) list -> Proof.context ->
     string list * Proof.context
   val add_fixes_cmd: (binding * string option * mixfix) list -> Proof.context ->
     string list * Proof.context
   val add_assms: Assumption.export ->
     (Thm.binding * (term * term list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val add_assms_cmd: Assumption.export ->
     (Thm.binding * (string * string list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val dest_cases: Proof.context option -> Proof.context -> (string * Rule_Cases.T) list
   val update_cases: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
   val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
   val check_case: Proof.context -> bool ->
     string * Position.T -> binding option list -> Rule_Cases.T
   val check_syntax_const: Proof.context -> string * Position.T -> string
   val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list ->
     Proof.context -> Proof.context
   val generic_syntax: bool -> Syntax.mode -> (string * typ * mixfix) list ->
     Context.generic -> Context.generic
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
   val generic_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
     Context.generic -> Context.generic
   val generic_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
     Context.generic -> Context.generic
   val type_alias: binding -> string -> Proof.context -> Proof.context
   val const_alias: binding -> string -> Proof.context -> Proof.context
   val add_const_constraint: string * typ option -> Proof.context -> Proof.context
   val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context
   val revert_abbrev: string -> string -> Proof.context -> Proof.context
   val generic_add_abbrev: string -> binding * term -> Context.generic ->
     (term * term) * Context.generic
   val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
   type stmt =
    {vars: ((binding * typ option * mixfix) * (string * term)) list,
     propss: term list list,
     binds: (indexname * term) list,
     result_binds: (indexname * term) list}
   val cert_stmt: (binding * typ option * mixfix) list -> (term * term list) list list ->
     Proof.context -> stmt * Proof.context
   val read_stmt: (binding * string option * mixfix) list -> (string * string list) list list ->
     Proof.context -> stmt * Proof.context
   type statement =
    {fixes: (string * term) list,
     assumes: term list list,
     shows: term list list,
     result_binds: (indexname * term option) list,
     text: term,
     result_text: term}
   val cert_statement: (binding * typ option * mixfix) list ->
     (term * term list) list list -> (term * term list) list list -> Proof.context ->
     statement * Proof.context
   val read_statement: (binding * string option * mixfix) list ->
     (string * string list) list list -> (string * string list) list list -> Proof.context ->
     statement * Proof.context
   val print_syntax: Proof.context -> unit
   val print_abbrevs: bool -> Proof.context -> unit
   val pretty_term_bindings: Proof.context -> Pretty.T list
   val pretty_local_facts: bool -> Proof.context -> Pretty.T list
   val print_local_facts: bool -> Proof.context -> unit
   val pretty_cases: Proof.context -> Pretty.T list
   val print_cases_proof: Proof.context -> Proof.context -> string
   val debug: bool Config.T
   val verbose: bool Config.T
   val pretty_ctxt: Proof.context -> Pretty.T list
   val pretty_context: Proof.context -> Pretty.T list
 end;
 
 structure Proof_Context: PROOF_CONTEXT =
 struct
 
 val theory_of = Proof_Context.theory_of;
 val init_global = Proof_Context.init_global;
 val get_global = Proof_Context.get_global;
 
 
 
 (** inner syntax mode **)
 
 datatype mode =
   Mode of
    {pattern: bool,             (*pattern binding schematic variables*)
     schematic: bool,           (*term referencing loose schematic variables*)
     abbrev: bool};             (*abbrev mode -- no normalization*)
 
 fun make_mode (pattern, schematic, abbrev) =
   Mode {pattern = pattern, schematic = schematic, abbrev = abbrev};
 
 val mode_default   = make_mode (false, false, false);
 val mode_pattern   = make_mode (true, false, false);
 val mode_schematic = make_mode (false, true, false);
 val mode_abbrev    = make_mode (false, false, true);
 
 
 
 (** Isar proof context information **)
 
 type cases = Rule_Cases.T Name_Space.table;
 val empty_cases: cases = Name_Space.empty_table Markup.caseN;
 
 datatype data =
   Data of
    {mode: mode,                  (*inner syntax mode*)
     syntax: Local_Syntax.T,      (*local syntax*)
     tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
     consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
     facts: Facts.T,              (*local facts, based on initial global facts*)
     cases: cases};               (*named case contexts*)
 
 fun make_data (mode, syntax, tsig, consts, facts, cases) =
   Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases};
 
 structure Data = Proof_Data
 (
   type T = data;
   fun init thy =
     make_data (mode_default,
       Local_Syntax.init thy,
       (Type.change_ignore (Sign.tsig_of thy), Sign.tsig_of thy),
       (Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy),
       Global_Theory.facts_of thy,
       empty_cases);
 );
 
 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
 
 fun map_data_result f ctxt =
   let
     val Data {mode, syntax, tsig, consts, facts, cases} = Data.get ctxt;
     val (res, data') = f (mode, syntax, tsig, consts, facts, cases) ||> make_data;
   in (res, Data.put data' ctxt) end;
 
 fun map_data f = snd o map_data_result (pair () o f);
 
 fun set_mode mode = map_data (fn (_, syntax, tsig, consts, facts, cases) =>
   (mode, syntax, tsig, consts, facts, cases));
 
 fun map_syntax f =
   map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
     (mode, f syntax, tsig, consts, facts, cases));
 
 fun map_syntax_idents f ctxt =
   let val (opt_idents', syntax') = f (#syntax (rep_data ctxt)) in
     ctxt
     |> map_syntax (K syntax')
     |> (case opt_idents' of NONE => I | SOME idents' => Syntax_Trans.put_idents idents')
   end;
 
 fun map_tsig f =
   map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
     (mode, syntax, f tsig, consts, facts, cases));
 
 fun map_consts f =
   map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
     (mode, syntax, tsig, f consts, facts, cases));
 
 fun map_facts_result f =
   map_data_result (fn (mode, syntax, tsig, consts, facts, cases) =>
     let val (res, facts') = f facts
     in (res, (mode, syntax, tsig, consts, facts', cases)) end);
 
 fun map_facts f = snd o map_facts_result (pair () o f);
 
 fun map_cases f =
   map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
     (mode, syntax, tsig, consts, facts, f cases));
 
 val get_mode = #mode o rep_data;
 val restore_mode = set_mode o get_mode;
 val abbrev_mode = get_mode #> (fn Mode {abbrev, ...} => abbrev);
 
 val syntax_of = #syntax o rep_data;
 val syn_of = Local_Syntax.syn_of o syntax_of;
 val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
 val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
 
 val tsig_of = #1 o #tsig o rep_data;
 val set_defsort = map_tsig o apfst o Type.set_defsort;
 fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
 fun arity_sorts ctxt = Type.arity_sorts (Context.Proof ctxt) (tsig_of ctxt);
 
 val consts_of = #1 o #consts o rep_data;
 val cases_of = #cases o rep_data;
 
 
 (* naming *)
 
 val naming_of = Name_Space.naming_of o Context.Proof;
 val map_naming = Context.proof_map o Name_Space.map_naming;
 val restore_naming = map_naming o K o naming_of;
 
 val full_name = Name_Space.full_name o naming_of;
 
 val get_scope = Name_Space.get_scope o naming_of;
 
 fun new_scope ctxt =
   let
     val (scope, naming') = Name_Space.new_scope (naming_of ctxt);
     val ctxt' = map_naming (K naming') ctxt;
   in (scope, ctxt') end;
 
 val private_scope = map_naming o Name_Space.private_scope;
 val private = map_naming o Name_Space.private;
 val qualified_scope = map_naming o Name_Space.qualified_scope;
 val qualified = map_naming o Name_Space.qualified;
 
 val concealed = map_naming Name_Space.concealed;
 
 
 (* name spaces *)
 
 val class_space = Type.class_space o tsig_of;
 val type_space = Type.type_space o tsig_of;
 val const_space = Consts.space_of o consts_of;
 
 fun defs_context ctxt = (ctxt, (const_space ctxt, type_space ctxt));
 
 val intern_class = Name_Space.intern o class_space;
 val intern_type = Name_Space.intern o type_space;
 val intern_const = Name_Space.intern o const_space;
 
 fun extern_class ctxt = Name_Space.extern ctxt (class_space ctxt);
 fun extern_type ctxt = Name_Space.extern ctxt (type_space ctxt);
 fun extern_const ctxt = Name_Space.extern ctxt (const_space ctxt);
 
 fun markup_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c |-> Markup.markup;
 fun markup_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c |-> Markup.markup;
 fun markup_const ctxt c = Name_Space.markup_extern ctxt (const_space ctxt) c |-> Markup.markup;
 
 fun pretty_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c |> Pretty.mark_str;
 fun pretty_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c |> Pretty.mark_str;
 fun pretty_const ctxt c = Name_Space.markup_extern ctxt (const_space ctxt) c |> Pretty.mark_str;
 
 
 (* theory transfer *)
 
 fun transfer_syntax thy ctxt = ctxt |>
   map_syntax (Local_Syntax.rebuild thy) |>
   map_tsig (fn tsig as (local_tsig, global_tsig) =>
     let val thy_tsig = Sign.tsig_of thy in
       if Type.eq_tsig (thy_tsig, global_tsig) then tsig
       else (Type.merge_tsig (Context.Proof ctxt) (local_tsig, thy_tsig), thy_tsig)  (*historic merge order*)
     end) |>
   map_consts (fn consts as (local_consts, global_consts) =>
     let val thy_consts = Sign.consts_of thy in
       if Consts.eq_consts (thy_consts, global_consts) then consts
       else (Consts.merge (local_consts, thy_consts), thy_consts)  (*historic merge order*)
     end);
 
 fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy;
 
 fun transfer_facts thy =
   map_facts (fn local_facts => Facts.merge (Global_Theory.facts_of thy, local_facts));
 
 fun background_theory f ctxt = transfer (f (theory_of ctxt)) ctxt;
 
 fun background_theory_result f ctxt =
   let val (res, thy') = f (theory_of ctxt)
   in (res, ctxt |> transfer thy') end;
 
 
 (* hybrid facts *)
 
 val facts_of = #facts o rep_data;
 
 fun facts_of_fact ctxt name =
   let
     val local_facts = facts_of ctxt;
     val global_facts = Global_Theory.facts_of (theory_of ctxt);
   in
     if Facts.defined local_facts name
     then local_facts else global_facts
   end;
 
 fun markup_extern_fact ctxt name =
   let
     val facts = facts_of_fact ctxt name;
     val (markup, xname) = Facts.markup_extern ctxt facts name;
     val markups =
       if Facts.is_dynamic facts name then [markup, Markup.dynamic_fact name]
       else [markup];
   in (markups, xname) end;
 
 
 (* augment context by implicit term declarations *)
 
 fun augment t ctxt = ctxt
   |> Variable.add_fixes_implicit t
   |> Variable.declare_term t
   |> Soft_Type_System.augment t;
 
 
 
 (** pretty printing **)
 
 val print_name = Token.print_name o Thy_Header.get_keywords';
 val pretty_name = Pretty.str oo print_name;
 
 fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
 
 fun pretty_fact_name ctxt a =
   Pretty.block [Pretty.marks_str (markup_extern_fact ctxt a), Pretty.str ":"];
 
 fun pretty_fact ctxt =
   let
     val pretty_thm = Thm.pretty_thm ctxt;
     val pretty_thms = map (Thm.pretty_thm_item ctxt);
   in
     fn ("", [th]) => pretty_thm th
      | ("", ths) => Pretty.blk (0, Pretty.fbreaks (pretty_thms ths))
      | (a, [th]) => Pretty.block [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm th]
      | (a, ths) => Pretty.block (Pretty.fbreaks (pretty_fact_name ctxt a :: pretty_thms ths))
   end;
 
 
 
 (** prepare types **)
 
 (* classes *)
 
 fun check_class ctxt (xname, pos) =
   let
     val tsig = tsig_of ctxt;
     val class_space = Type.class_space tsig;
 
     val name = Type.cert_class tsig (Name_Space.intern class_space xname)
       handle TYPE (msg, _, _) =>
         error (msg ^ Position.here pos ^
           Completion.markup_report
             [Name_Space.completion (Context.Proof ctxt) class_space (K true) (xname, pos)]);
     val reports =
       if Context_Position.is_reported ctxt pos
       then [(pos, Name_Space.markup class_space name)] else [];
   in (name, reports) end;
 
 fun read_class ctxt text =
   let
     val source = Syntax.read_input text;
     val (c, reports) = check_class ctxt (Input.source_content source);
     val _ = Context_Position.reports ctxt reports;
   in c end;
 
 
 (* types *)
 
 fun read_typ_mode mode ctxt s =
   Syntax.read_typ (Type.set_mode mode ctxt) s;
 
 val read_typ = read_typ_mode Type.mode_default;
 val read_typ_syntax = read_typ_mode Type.mode_syntax;
 val read_typ_abbrev = read_typ_mode Type.mode_abbrev;
 
 
 fun cert_typ_mode mode ctxt T =
   Type.cert_typ_mode mode (tsig_of ctxt) T
     handle TYPE (msg, _, _) => error msg;
 
 val cert_typ = cert_typ_mode Type.mode_default;
 val cert_typ_syntax = cert_typ_mode Type.mode_syntax;
 val cert_typ_abbrev = cert_typ_mode Type.mode_abbrev;
 
 
 
 (** prepare terms and propositions **)
 
 (* inferred types of parameters *)
 
 fun infer_type ctxt x =
   Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x));
 
 fun inferred_param x ctxt =
   let val p = (x, infer_type ctxt (x, dummyT))
   in (p, ctxt |> Variable.declare_term (Free p)) end;
 
 fun inferred_fixes ctxt =
   fold_map inferred_param (map #2 (Variable.dest_fixes ctxt)) ctxt;
 
 
 (* type names *)
 
 fun check_type_name {proper, strict} ctxt (c, pos) =
   if Lexicon.is_tid c then
     if proper then error ("Not a type constructor: " ^ quote c ^ Position.here pos)
     else
       let
         val reports =
           if Context_Position.is_reported ctxt pos
           then [(pos, Markup.tfree)] else [];
       in (TFree (c, default_sort ctxt (c, ~1)), reports) end
   else
     let
       val ((d, reports), decl) = Type.check_decl (Context.Proof ctxt) (tsig_of ctxt) (c, pos);
       fun err () = error ("Bad type name: " ^ quote d ^ Position.here pos);
       val args =
         (case decl of
           Type.LogicalType n => n
         | Type.Abbreviation (vs, _, _) => if strict then err () else length vs
         | Type.Nonterminal => if strict then err () else 0);
     in (Type (d, replicate args dummyT), reports) end;
 
 fun read_type_name flags ctxt text =
   let
     val source = Syntax.read_input text;
     val (T, reports) = check_type_name flags ctxt (Input.source_content source);
     val _ = Context_Position.reports ctxt reports;
   in T end;
 
 
 (* constant names *)
 
 fun consts_completion_message ctxt (c, ps) =
   ps |> map (fn pos =>
     Name_Space.completion (Context.Proof ctxt) (Consts.space_of (consts_of ctxt)) (K true) (c, pos))
   |> Completion.markup_report;
 
 fun check_const {proper, strict} ctxt (c, ps) =
   let
     val _ =
       Name.reject_internal (c, ps) handle ERROR msg =>
         error (msg ^ consts_completion_message ctxt (c, ps));
     fun err msg = error (msg ^ Position.here_list ps);
     val consts = consts_of ctxt;
     val fixed = if proper then NONE else Variable.lookup_fixed ctxt c;
     val (t, reports) =
       (case (fixed, Variable.lookup_const ctxt c) of
         (SOME x, NONE) =>
           let
             val reports = ps
               |> filter (Context_Position.is_reported ctxt)
               |> map (fn pos =>
                 (pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free)));
           in (Free (x, infer_type ctxt (x, dummyT)), reports) end
       | (_, SOME d) =>
           let
             val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg;
             val reports = ps
               |> filter (Context_Position.is_reported ctxt)
               |> map (fn pos => (pos, Name_Space.markup (Consts.space_of consts) d));
           in (Const (d, T), reports) end
       | _ => Consts.check_const (Context.Proof ctxt) consts (c, ps));
     val _ =
       (case (strict, t) of
         (true, Const (d, _)) =>
           (ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg)
       | _ => ());
   in (t, reports) end;
 
 fun read_const flags ctxt text =
   let
     val source = Syntax.read_input text;
     val (c, pos) = Input.source_content source;
     val (t, reports) = check_const flags ctxt (c, [pos]);
     val _ = Context_Position.reports ctxt reports;
   in t end;
 
 
 (* type arities *)
 
 local
 
 fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
   let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
   in Type.add_arity (Context.Proof ctxt) arity (tsig_of ctxt); arity end;
 
 in
 
 val read_arity =
   prep_arity ((#1 o dest_Type) oo read_type_name {proper = true, strict = true}) Syntax.read_sort;
 
 val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
 
 end;
 
 
 (* read_term *)
 
 fun read_term_mode mode ctxt = Syntax.read_term (set_mode mode ctxt);
 
 val read_term_pattern   = read_term_mode mode_pattern;
 val read_term_schematic = read_term_mode mode_schematic;
 val read_term_abbrev    = read_term_mode mode_abbrev;
 
 
 (* local abbreviations *)
 
 local
 
 fun certify_consts ctxt =
   Consts.certify (Context.Proof ctxt) (tsig_of ctxt)
     (not (abbrev_mode ctxt)) (consts_of ctxt);
 
 fun expand_binds ctxt =
   let
     val Mode {pattern, schematic, ...} = get_mode ctxt;
 
     fun reject_schematic (t as Var _) =
           error ("Unbound schematic variable: " ^ Syntax.string_of_term ctxt t)
       | reject_schematic (Abs (_, _, t)) = reject_schematic t
       | reject_schematic (t $ u) = (reject_schematic t; reject_schematic u)
       | reject_schematic _ = ();
   in
     if pattern then I
     else Variable.expand_binds ctxt #> (if schematic then I else tap reject_schematic)
   end;
 
 in
 
 fun expand_abbrevs ctxt = certify_consts ctxt #> expand_binds ctxt;
 
 end;
 
 val show_abbrevs = Config.declare_bool ("show_abbrevs", \<^here>) (K true);
 
 fun contract_abbrevs ctxt t =
   let
     val thy = theory_of ctxt;
     val consts = consts_of ctxt;
     val Mode {abbrev, ...} = get_mode ctxt;
     val retrieve = Consts.retrieve_abbrevs consts (print_mode_value () @ [""]);
     fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u) (retrieve u));
   in
     if abbrev orelse not (Config.get ctxt show_abbrevs) orelse not (can Term.type_of t) then t
     else Pattern.rewrite_term_top thy [] [match_abbrev] t
   end;
 
 
 (* patterns *)
 
 fun prepare_patternT ctxt T =
   let
     val Mode {pattern, schematic, ...} = get_mode ctxt;
     val _ =
       pattern orelse schematic orelse
         T |> Term.exists_subtype
           (fn T as TVar (xi, _) =>
             not (Type_Infer.is_param xi) andalso
               error ("Illegal schematic type variable: " ^ Syntax.string_of_typ ctxt T)
           | _ => false)
   in T end;
 
 
 local
 
 val dummies = Config.declare_bool ("Proof_Context.dummies", \<^here>) (K false);
 
 fun check_dummies ctxt t =
   if Config.get ctxt dummies then t
   else Term.no_dummy_patterns t handle TERM _ => error "Illegal dummy pattern(s) in term";
 
 fun prepare_dummies ts = #1 (fold_map Term.replace_dummy_patterns ts 1);
 
 in
 
 val allow_dummies = Config.put dummies true;
 
 fun prepare_patterns ctxt =
   let val Mode {pattern, ...} = get_mode ctxt in
     Type_Infer.fixate ctxt pattern #>
     pattern ? Variable.polymorphic ctxt #>
     (map o Term.map_types) (prepare_patternT ctxt) #>
     (if pattern then prepare_dummies else map (check_dummies ctxt))
   end;
 
 end;
 
 
 (* sort constraints *)
 
 local
 
 fun prepare_sorts_env ctxt tys =
   let
     val tsig = tsig_of ctxt;
     val defaultS = Type.defaultS tsig;
 
     val dummy_var = ("'_dummy_", ~1);
 
     fun constraint (xi, raw_S) env =
       let val (ps, S) = Term_Position.decode_positionS raw_S in
         if xi = dummy_var orelse S = dummyS then env
         else
           Vartab.insert (op =) (xi, Type.minimize_sort tsig S) env
             handle Vartab.DUP _ =>
               error ("Inconsistent sort constraints for type variable " ^
                 quote (Term.string_of_vname' xi) ^ Position.here_list ps)
       end;
 
     val env =
       Vartab.build (tys |> (fold o fold_atyps)
         (fn TFree (x, S) => constraint ((x, ~1), S)
           | TVar v => constraint v
           | _ => I));
 
     fun get_sort xi raw_S =
       if xi = dummy_var then
         Type.minimize_sort tsig (#2 (Term_Position.decode_positionS raw_S))
       else
         (case (Vartab.lookup env xi, Variable.def_sort ctxt xi) of
           (NONE, NONE) => defaultS
         | (NONE, SOME S) => S
         | (SOME S, NONE) => S
         | (SOME S, SOME S') =>
             if Type.eq_sort tsig (S, S') then S'
             else
               error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^
                 " inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^
                 " for type variable " ^ quote (Term.string_of_vname' xi)));
 
     fun add_report S pos reports =
       if Position.is_reported pos andalso not (AList.defined (op =) reports pos) then
         (pos, Position.reported_text pos Markup.sorting (Syntax.string_of_sort ctxt S)) :: reports
       else reports;
 
     fun get_sort_reports xi raw_S =
       let
         val ps = #1 (Term_Position.decode_positionS raw_S);
         val S = get_sort xi raw_S handle ERROR msg => error (msg ^ Position.here_list ps);
       in fold (add_report S) ps end;
 
     val reports =
       (fold o fold_atyps)
         (fn T =>
           if Term_Position.is_positionT T then I
           else
             (case T of
               TFree (x, raw_S) => get_sort_reports (x, ~1) raw_S
             | TVar (xi, raw_S) => get_sort_reports xi raw_S
             | _ => I)) tys [];
 
   in (map #2 reports, get_sort) end;
 
 fun replace_sortsT get_sort =
   map_atyps
     (fn T =>
       if Term_Position.is_positionT T then T
       else
         (case T of
           TFree (x, raw_S) => TFree (x, get_sort (x, ~1) raw_S)
         | TVar (xi, raw_S) => TVar (xi, get_sort xi raw_S)
         | _ => T));
 
 in
 
 fun prepare_sortsT ctxt tys =
   let val (sorting_report, get_sort) = prepare_sorts_env ctxt tys
   in (sorting_report, map (replace_sortsT get_sort) tys) end;
 
 fun prepare_sorts ctxt tms =
   let
     val tys = rev ((fold o fold_types) cons tms []);
     val (sorting_report, get_sort) = prepare_sorts_env ctxt tys;
   in (sorting_report, (map o map_types) (replace_sortsT get_sort) tms) end;
 
 fun check_tfree ctxt v =
   let
     val (sorting_report, [TFree a]) = prepare_sortsT ctxt [TFree v];
     val _ = if Context_Position.reports_enabled ctxt then Output.report sorting_report else ();
   in a end;
 
 end;
 
 
 (* certify terms *)
 
 local
 
 fun gen_cert prop ctxt t =
   t
   |> expand_abbrevs ctxt
   |> (fn t' =>
       #1 (Sign.certify' prop (Context.Proof ctxt) false (consts_of ctxt) (theory_of ctxt) t')
         handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg);
 
 in
 
 val cert_term = gen_cert false;
 val cert_prop = gen_cert true;
 
 end;
 
 
 (* check/uncheck *)
 
 fun def_type ctxt =
   let val Mode {pattern, ...} = get_mode ctxt
   in Variable.def_type ctxt pattern end;
 
 fun standard_typ_check ctxt =
   map (cert_typ_mode (Type.get_mode ctxt) ctxt #> prepare_patternT ctxt);
 
 val standard_term_check_finish = prepare_patterns;
 
 fun standard_term_uncheck ctxt = map (contract_abbrevs ctxt);
 
 
 
 (** export results **)
 
 fun common_export is_goal inner outer =
   map (Assumption.export is_goal inner outer) #>
   Variable.export inner outer;
 
 val goal_export = common_export true;
 val export = common_export false;
 
 fun export_morphism inner outer =
   Assumption.export_morphism inner outer $>
   Variable.export_morphism inner outer;
 
-fun norm_export_morphism inner outer =
-  export_morphism inner outer $>
-  Morphism.thm_morphism "Proof_Context.norm_export" Goal.norm_result_without_context;
-
 
 
 (** term bindings **)
 
 (* auto bindings *)
 
 fun auto_bind f props ctxt = fold Variable.maybe_bind_term (f ctxt props) ctxt;
 
 val auto_bind_goal = auto_bind Auto_Bind.goal;
 val auto_bind_facts = auto_bind Auto_Bind.facts;
 
 
 (* match bindings *)
 
 fun simult_matches ctxt (t, pats) =
   (case Seq.pull (Unify.matchers (Context.Proof ctxt) (map (rpair t) pats)) of
     NONE => error "Pattern match failed!"
   | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []);
 
 fun maybe_bind_term (xi, t) ctxt =
   ctxt
   |> Variable.maybe_bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t);
 
 val bind_term = maybe_bind_term o apsnd SOME;
 
 
 (* propositions with patterns *)
 
 local
 
 fun prep_propp prep_props ctxt raw_args =
   let
     val props = prep_props ctxt (maps (map fst) raw_args);
     val props_ctxt = fold Variable.declare_term props ctxt;
     val patss = maps (map (prep_props (set_mode mode_pattern props_ctxt) o snd)) raw_args;
 
     val propps = unflat raw_args (props ~~ patss);
     val binds = (maps o maps) (simult_matches props_ctxt) propps;
   in (map (map fst) propps, binds) end;
 
 in
 
 val cert_propp = prep_propp (map o cert_prop);
 val read_propp = prep_propp Syntax.read_props;
 
 end;
 
 
 
 (** theorems **)
 
 (* fact_tac *)
 
 local
 
 fun comp_hhf_tac ctxt th i st =
   PRIMSEQ (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
     (false, Drule.lift_all ctxt (Thm.cprem_of st i) th, 0) i) st;
 
 fun comp_incr_tac _ [] _ = no_tac
   | comp_incr_tac ctxt (th :: ths) i =
       (fn st => comp_hhf_tac ctxt (Drule.incr_indexes st th) i st) APPEND
       comp_incr_tac ctxt ths i;
 
 val vacuous_facts = [Drule.termI];
 
 in
 
 fun potential_facts ctxt prop =
   let
     val body = Term.strip_all_body prop;
     val vacuous =
       filter (fn th => Term.could_unify (body, Thm.concl_of th)) vacuous_facts
       |> map (rpair Position.none);
   in Facts.could_unify (facts_of ctxt) body @ vacuous end;
 
 fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac ctxt facts;
 
 fun some_fact_tac ctxt =
   SUBGOAL (fn (goal, i) => fact_tac ctxt (map #1 (potential_facts ctxt goal)) i);
 
 end;
 
 
 (* lookup facts *)
 
 fun lookup_fact ctxt name =
   let
     val context = Context.Proof ctxt;
     val thy = Proof_Context.theory_of ctxt;
   in
     (case Facts.lookup context (facts_of ctxt) name of
       NONE => Facts.lookup context (Global_Theory.facts_of thy) name
     | some => some)
   end;
 
 
 (* retrieve facts *)
 
 val dynamic_facts_dummy = Config.declare_bool ("dynamic_facts_dummy_", \<^here>) (K false);
 
 local
 
 fun retrieve_global context =
   Facts.retrieve context (Global_Theory.facts_of (Context.theory_of context));
 
 fun retrieve_generic (context as Context.Proof ctxt) arg =
       (Facts.retrieve context (facts_of ctxt) arg handle ERROR local_msg =>
         (retrieve_global context arg handle ERROR _ => error local_msg))
   | retrieve_generic context arg = retrieve_global context arg;
 
 fun retrieve pick context (Facts.Fact s) =
       let
         val ctxt = Context.the_proof context;
         val pos = Syntax.read_input_pos s;
         val prop =
           Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s
           |> singleton (Variable.polymorphic ctxt);
         fun err ps msg =
           error (msg ^ Position.here_list (pos :: ps) ^ ":\n" ^ Syntax.string_of_term ctxt prop);
 
         val (prop', _) = Term.replace_dummy_patterns prop (Variable.maxidx_of ctxt + 1);
         fun prove th = Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th])));
         val results = map_filter (try (apfst prove)) (potential_facts ctxt prop');
         val (thm, thm_pos) =
           (case distinct (eq_fst Thm.eq_thm_prop) results of
             [res] => res
           | [] => err [] "Failed to retrieve literal fact"
           | dups => err (distinct (op =) (map #2 dups)) "Ambiguous specification of literal fact");
 
         val markup = Position.entity_markup Markup.literal_factN ("", thm_pos);
         val _ = Context_Position.report_generic context pos markup;
       in pick true ("", thm_pos) [thm] end
   | retrieve pick context (Facts.Named ((xname, pos), sel)) =
       let
         val thy = Context.theory_of context;
         fun immediate thms = {name = xname, dynamic = false, thms = map (Thm.transfer thy) thms};
         val {name, dynamic, thms} =
           (case xname of
             "" => immediate [Drule.dummy_thm]
           | "_" => immediate [Drule.asm_rl]
           | "nothing" => immediate []
           | _ => retrieve_generic context (xname, pos));
         val thms' =
           if dynamic andalso Config.get_generic context dynamic_facts_dummy
           then [Drule.free_dummy_thm]
           else Facts.select (Facts.Named ((name, pos), sel)) thms;
       in pick (dynamic andalso is_none sel) (name, pos) thms' end;
 
 in
 
 val get_fact_generic =
   retrieve (fn dynamic => fn (name, _) => fn thms =>
     (if dynamic then SOME name else NONE, thms));
 
 val get_fact = retrieve (K (K I)) o Context.Proof;
 val get_fact_single = retrieve (K Facts.the_single) o Context.Proof;
 
 fun get_thms ctxt = get_fact ctxt o Facts.named;
 fun get_thm ctxt = get_fact_single ctxt o Facts.named;
 
 end;
 
 
 (* inner statement mode *)
 
 val inner_stmt = Config.declare_bool ("inner_stmt", \<^here>) (K false);
 fun is_stmt ctxt = Config.get ctxt inner_stmt;
 val set_stmt = Config.put inner_stmt;
 val restore_stmt = set_stmt o is_stmt;
 
 
 (* facts *)
 
 fun add_thms_dynamic arg ctxt =
   ctxt |> map_facts_result (Facts.add_dynamic (Context.Proof ctxt) arg);
 
 local
 
 fun add_facts {index} arg ctxt = ctxt
   |> map_facts_result (Facts.add_static (Context.Proof ctxt) {strict = false, index = index} arg);
 
 fun update_facts flags (b, SOME ths) ctxt = ctxt |> add_facts flags (b, Lazy.value ths) |> #2
   | update_facts _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b));
 
 fun bind_name ctxt b = (full_name ctxt b, Binding.default_pos_of b);
 
 in
 
 fun add_thms_lazy kind (b, ths) ctxt =
   let
     val name_pos = bind_name ctxt b;
     val ths' =
       Global_Theory.check_thms_lazy ths
       |> Lazy.map_finished
           (Global_Theory.name_thms Global_Theory.unofficial1 name_pos #> map (Thm.kind_rule kind));
     val (_, ctxt') = add_facts {index = is_stmt ctxt} (b, ths') ctxt;
   in ctxt' end;
 
 fun note_thms kind ((b, more_atts), facts) ctxt =
   let
     val (name, pos) = bind_name ctxt b;
     val facts' = facts
       |> Global_Theory.burrow_fact (Global_Theory.name_thms Global_Theory.unofficial1 (name, pos));
     fun app (ths, atts) =
       fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
     val (res, ctxt') = fold_map app facts' ctxt;
     val thms = Global_Theory.name_thms Global_Theory.unofficial2 (name, pos) (flat res);
     val (_, ctxt'') = ctxt' |> add_facts {index = is_stmt ctxt} (b, Lazy.value thms);
   in ((name, thms), ctxt'') end;
 
 val note_thmss = fold_map o note_thms;
 
 fun put_thms index thms ctxt = ctxt
   |> map_naming (K Name_Space.local_naming)
   |> Context_Position.set_visible false
   |> update_facts {index = index} (apfst Binding.name thms)
   |> Context_Position.restore_visible ctxt
   |> restore_naming ctxt;
 
 end;
 
 fun alias_fact b c ctxt = map_facts (Facts.alias (naming_of ctxt) b c) ctxt;
 
 
 
 (** basic logical entities **)
 
 (* variables *)
 
 fun declare_var (x, opt_T, mx) ctxt =
   let val T = (case opt_T of SOME T => T | NONE => Mixfix.default_constraint mx)
   in (T, ctxt |> Variable.declare_constraints (Free (x, T))) end;
 
 fun add_syntax vars ctxt =
   map_syntax_idents (Local_Syntax.add_syntax ctxt (map (pair Local_Syntax.Fixed) vars)) ctxt;
 
 fun check_var internal b =
   let
     val x = Variable.check_name b;
     val check = if internal then Name.reject_skolem else Name.reject_internal;
     val _ =
       if can check (x, []) andalso Symbol_Pos.is_identifier x then ()
       else error ("Bad name: " ^ Binding.print b);
   in x end;
 
 local
 
 fun check_mixfix ctxt (b, T, mx) =
   let
     val ([x], ctxt') = Variable.add_fixes_binding [Binding.reset_pos b] ctxt;
     val mx' = Mixfix.reset_pos mx;
     val _ = add_syntax [(x, T, if Context_Position.reports_enabled ctxt then mx else mx')] ctxt';
   in mx' end;
 
 fun prep_var prep_typ internal (b, raw_T, mx) ctxt =
   let
     val x = check_var internal b;
     fun cond_tvars T =
       if internal then T
       else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
     val opt_T = Option.map (cond_tvars o prep_typ ctxt) raw_T;
     val (T, ctxt') = ctxt |> declare_var (x, opt_T, mx);
     val mx' = if Mixfix.is_empty mx then mx else check_mixfix ctxt' (b, T, mx);
   in ((b, SOME T, mx'), ctxt') end;
 
 in
 
 val read_var = prep_var Syntax.read_typ false;
 val cert_var = prep_var cert_typ true;
 
 end;
 
 
 (* syntax *)
 
 fun check_syntax_const ctxt (c, pos) =
   if is_some (Syntax.lookup_const (syn_of ctxt) c) then c
   else error ("Unknown syntax const: " ^ quote c ^ Position.here pos);
 
 fun syntax add mode args ctxt =
   let val args' = map (pair Local_Syntax.Const) args
   in ctxt |> map_syntax (#2 o Local_Syntax.update_modesyntax ctxt add mode args') end;
 
 fun generic_syntax add mode args =
   Context.mapping (Sign.syntax add mode args) (syntax add mode args);
 
 
 (* notation *)
 
 local
 
 fun type_syntax (Type (c, args), mx) =
       SOME (Local_Syntax.Type, (Lexicon.mark_type c, Mixfix.make_type (length args), mx))
   | type_syntax _ = NONE;
 
 fun const_syntax _ (Free (x, T), mx) = SOME (Local_Syntax.Fixed, (x, T, mx))
   | const_syntax ctxt (Const (c, _), mx) =
       (case try (Consts.type_scheme (consts_of ctxt)) c of
         SOME T => SOME (Local_Syntax.Const, (Lexicon.mark_const c, T, mx))
       | NONE => NONE)
   | const_syntax _ _ = NONE;
 
 fun gen_notation make_syntax add mode args ctxt =
   ctxt |> map_syntax_idents
     (Local_Syntax.update_modesyntax ctxt add mode (map_filter (make_syntax ctxt) args));
 
 in
 
 val type_notation = gen_notation (K type_syntax);
 val notation = gen_notation const_syntax;
 
 fun generic_type_notation add mode args phi =
   let
     val args' = args |> map_filter (fn (T, mx) =>
       let
         val T' = Morphism.typ phi T;
         val similar = (case (T, T') of (Type (c, _), Type (c', _)) => c = c' | _ => false);
       in if similar then SOME (T', mx) else NONE end);
   in Context.mapping (Sign.type_notation add mode args') (type_notation add mode args') end;
 
 fun generic_notation add mode args phi =
   let
     val args' = args |> map_filter (fn (t, mx) =>
       let val t' = Morphism.term phi t
       in if Term.aconv_untyped (t, t') then SOME (t', mx) else NONE end);
   in Context.mapping (Sign.notation add mode args') (notation add mode args') end;
 
 end;
 
 
 (* aliases *)
 
 fun type_alias b c ctxt = (map_tsig o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt;
 fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt;
 
 
 (* local constants *)
 
 fun add_const_constraint (c, opt_T) ctxt =
   let
     fun prepT raw_T =
       let val T = cert_typ ctxt raw_T
       in cert_term ctxt (Const (c, T)); T end;
   in ctxt |> (map_consts o apfst) (Consts.constrain (c, Option.map prepT opt_T)) end;
 
 fun add_abbrev mode (b, raw_t) ctxt =
   let
     val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b);
     val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
     val ((lhs, rhs), consts') = consts_of ctxt
       |> Consts.abbreviate (Context.Proof ctxt) (tsig_of ctxt) mode (b, t);
   in
     ctxt
     |> (map_consts o apfst) (K consts')
     |> Variable.declare_term rhs
     |> pair (lhs, rhs)
   end;
 
 fun revert_abbrev mode c = (map_consts o apfst) (Consts.revert_abbrev mode c);
 
 fun generic_add_abbrev mode arg =
   Context.mapping_result (Sign.add_abbrev mode arg) (add_abbrev mode arg);
 
 fun generic_revert_abbrev mode arg =
   Context.mapping (Sign.revert_abbrev mode arg) (revert_abbrev mode arg);
 
 
 (* fixes *)
 
 local
 
 fun gen_fixes prep_var raw_vars ctxt =
   let
     val (vars, _) = fold_map prep_var raw_vars ctxt;
     val (xs, ctxt') = Variable.add_fixes_binding (map #1 vars) ctxt;
     val _ =
       Context_Position.reports ctxt'
         (flat (map2 (fn x => fn pos =>
           [(pos, Variable.markup ctxt' x), (pos, Variable.markup_entity_def ctxt' x)])
             xs (map (Binding.pos_of o #1) vars)));
     val vars' = map2 (fn x => fn (_, opt_T, mx) => (x, opt_T, mx)) xs vars;
     val (Ts, ctxt'') = fold_map declare_var vars' ctxt';
     val vars'' = map2 (fn T => fn (x, _, mx) => (x, T, mx)) Ts vars';
   in (xs, add_syntax vars'' ctxt'') end;
 
 in
 
 val add_fixes = gen_fixes cert_var;
 val add_fixes_cmd = gen_fixes read_var;
 
 end;
 
 
 
 (** assumptions **)
 
 local
 
 fun gen_assms prep_propp exp args ctxt =
   let
     val (propss, binds) = prep_propp ctxt (map snd args);
     val props = flat propss;
   in
     ctxt
     |> fold Variable.declare_term props
     |> tap (Variable.warn_extra_tfrees ctxt)
     |> fold_burrow (Assumption.add_assms exp o map (Thm.cterm_of ctxt)) propss
     |-> (fn premss =>
       auto_bind_facts props
       #> fold Variable.bind_term binds
       #> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss))
   end;
 
 in
 
 val add_assms = gen_assms cert_propp;
 val add_assms_cmd = gen_assms read_propp;
 
 end;
 
 
 
 (** cases **)
 
 fun dest_cases prev_ctxt ctxt =
   let
     val serial_of = #serial oo (Name_Space.the_entry o Name_Space.space_of_table);
     val ignored =
       (case prev_ctxt of
         NONE => Intset.empty
       | SOME ctxt0 =>
           let val cases0 = cases_of ctxt0 in
             Intset.build (cases0 |> Name_Space.fold_table (fn (a, _) =>
               Intset.insert (serial_of cases0 a)))
           end);
      val cases = cases_of ctxt;
   in
     Name_Space.fold_table (fn (a, c) =>
       let val i = serial_of cases a
       in not (Intset.member ignored i) ? cons (i, (a, c)) end) cases []
     |> sort (int_ord o apply2 #1) |> map #2
   end;
 
 local
 
 fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
   | drop_schematic b = b;
 
 fun update_case _ ("", _) cases = cases
   | update_case _ (name, NONE) cases = Name_Space.del_table name cases
   | update_case context (name, SOME c) cases =
       #2 (Name_Space.define context false (Binding.name name, c) cases);
 
 fun fix (b, T) ctxt =
   let val ([x], ctxt') = add_fixes [(b, SOME T, NoSyn)] ctxt
   in (Free (x, T), ctxt') end;
 
 in
 
 fun update_cases args ctxt =
   let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming);
   in map_cases (fold (update_case context) args) ctxt end;
 
 fun case_result c ctxt =
   let
     val Rule_Cases.Case {fixes, ...} = c;
     val (ts, ctxt') = ctxt |> fold_map fix fixes;
     val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c;
   in
     ctxt'
     |> fold (maybe_bind_term o drop_schematic) binds
     |> update_cases (map (apsnd SOME) cases)
     |> pair (assumes, (binds, cases))
   end;
 
 val apply_case = apfst fst oo case_result;
 
 fun check_case ctxt internal (name, pos) param_specs =
   let
     val (_, Rule_Cases.Case {fixes, assumes, binds, cases}) =
       Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos);
 
     val _ = List.app (fn NONE => () | SOME b => ignore (check_var internal b)) param_specs;
     fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
       | replace [] ys = ys
       | replace (_ :: _) [] =
           error ("Too many parameters for case " ^ quote name ^ Position.here pos);
     val fixes' = replace param_specs fixes;
     val binds' = map drop_schematic binds;
   in
     if null (fold (Term.add_tvarsT o snd) fixes []) andalso
       null (fold (fold Term.add_vars o snd) assumes []) then
         Rule_Cases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases}
     else error ("Illegal schematic variable(s) in case " ^ quote name ^ Position.here pos)
   end;
 
 end;
 
 
 (* structured statements *)
 
 type stmt =
  {vars: ((binding * typ option * mixfix) * (string * term)) list,
   propss: term list list,
   binds: (indexname * term) list,
   result_binds: (indexname * term) list};
 
 type statement =
  {fixes: (string * term) list,
   assumes: term list list,
   shows: term list list,
   result_binds: (indexname * term option) list,
   text: term,
   result_text: term};
 
 local
 
 fun export_binds ctxt' ctxt params binds =
   let
     val rhss =
       map (the_list o Option.map (Logic.close_term params) o snd) binds
       |> burrow (Variable.export_terms ctxt' ctxt)
       |> map (try the_single);
   in map fst binds ~~ rhss end;
 
 fun prep_stmt prep_var prep_propp raw_vars raw_propps ctxt =
   let
     val (vars, vars_ctxt) = fold_map prep_var raw_vars ctxt;
     val xs = map (Variable.check_name o #1) vars;
     val (xs', fixes_ctxt) = add_fixes vars vars_ctxt;
 
     val (propss, binds) = prep_propp fixes_ctxt raw_propps;
     val (ps, params_ctxt) = fixes_ctxt
       |> (fold o fold) Variable.declare_term propss
       |> fold_map inferred_param xs';
     val params = xs ~~ map Free ps;
 
     val vars' = map2 (fn (b, _, mx) => fn (_, T) => (b, SOME T, mx)) vars ps;
     val binds' = binds
       |> map (apsnd SOME)
       |> export_binds params_ctxt ctxt params
       |> map (apsnd the);
 
     val _ = Variable.warn_extra_tfrees fixes_ctxt params_ctxt;
     val result : stmt =
       {vars = vars' ~~ params, propss = propss, binds = binds, result_binds = binds'};
   in (result, params_ctxt) end;
 
 fun prep_statement prep_var prep_propp raw_fixes raw_assumes raw_shows ctxt =
   let
     val ((fixes, (assumes, shows), binds), ctxt') = ctxt
       |> prep_stmt prep_var prep_propp raw_fixes (raw_assumes @ raw_shows)
       |-> (fn {vars, propss, binds, ...} =>
         fold Variable.bind_term binds #>
         pair (map #2 vars, chop (length raw_assumes) propss, binds));
     val binds' =
       (Auto_Bind.facts ctxt' (flat shows) @
         (case try List.last (flat shows) of
           NONE => []
         | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds))
       |> export_binds ctxt' ctxt fixes;
 
     val text = Logic.close_prop fixes (flat assumes) (Logic.mk_conjunction_list (flat shows));
     val text' = singleton (Variable.export_terms ctxt' ctxt) text;
 
     val result : statement =
      {fixes = fixes,
       assumes = assumes,
       shows = shows,
       result_binds = binds',
       text = text,
       result_text = text'};
   in (result, ctxt') end;
 
 in
 
 val cert_stmt = prep_stmt cert_var cert_propp;
 val read_stmt = prep_stmt read_var read_propp;
 val cert_statement = prep_statement cert_var cert_propp;
 val read_statement = prep_statement read_var read_propp;
 
 end;
 
 
 
 (** print context information **)
 
 (* local syntax *)
 
 val print_syntax = Syntax.print_syntax o syn_of;
 
 
 (* abbreviations *)
 
 fun pretty_abbrevs verbose show_globals ctxt =
   let
     val space = const_space ctxt;
     val (constants, global_constants) =
       apply2 (#constants o Consts.dest) (#consts (rep_data ctxt));
     val globals = Symtab.make global_constants;
     fun add_abbr (_, (_, NONE)) = I
       | add_abbr (c, (T, SOME t)) =
           if not show_globals andalso Symtab.defined globals c then I
           else cons (c, Logic.mk_equals (Const (c, T), t));
     val abbrevs = Name_Space.markup_entries verbose ctxt space (fold add_abbr constants []);
   in
     if null abbrevs then []
     else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]
   end;
 
 fun print_abbrevs verbose = Pretty.writeln_chunks o pretty_abbrevs verbose true;
 
 
 (* term bindings *)
 
 fun pretty_term_bindings ctxt =
   let
     val binds = Variable.binds_of ctxt;
     fun prt_bind (xi, (T, t)) = pretty_term_abbrev ctxt (Logic.mk_equals (Var (xi, T), t));
   in
     if Vartab.is_empty binds then []
     else [Pretty.big_list "term bindings:" (map prt_bind (Vartab.dest binds))]
   end;
 
 
 (* local facts *)
 
 fun pretty_local_facts verbose ctxt =
   let
     val facts = facts_of ctxt;
     val props = map #1 (Facts.props facts);
     val local_facts =
       (if null props then [] else [("<unnamed>", props)]) @
       Facts.dest_static verbose [Global_Theory.facts_of (theory_of ctxt)] facts;
   in
     if null local_facts then []
     else
       [Pretty.big_list "local facts:"
         (map #1 (sort_by (#1 o #2) (map (`(pretty_fact ctxt)) local_facts)))]
   end;
 
 fun print_local_facts verbose ctxt =
   Pretty.writeln_chunks (pretty_local_facts verbose ctxt);
 
 
 (* named local contexts *)
 
 local
 
 fun pretty_case (name, (fixes, ((asms, (lets, cs)), ctxt))) =
   let
     val prt_name = pretty_name ctxt;
     val prt_term = Syntax.pretty_term ctxt;
 
     fun prt_let (xi, t) = Pretty.block
       [Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1,
         Pretty.quote (prt_term t)];
 
     fun prt_asm (a, ts) =
       Pretty.block (Pretty.breaks
         ((if a = "" then [] else [prt_name a, Pretty.str ":"]) @
           map (Pretty.quote o prt_term) ts));
 
     fun prt_sect _ _ _ [] = []
       | prt_sect head sep prt xs =
           [Pretty.block (Pretty.breaks (head ::
             flat (separate sep (map (single o prt) xs))))];
   in
     Pretty.block
       (prt_name name :: Pretty.str ":" :: Pretty.fbrk ::
         Pretty.fbreaks
           (prt_sect (Pretty.keyword1 "fix") [] (prt_name o Binding.name_of o fst) fixes @
            prt_sect (Pretty.keyword1 "let") [Pretty.keyword2 "and"] prt_let
              (map_filter (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @
            (if forall (null o #2) asms then []
             else prt_sect (Pretty.keyword1 "assume") [Pretty.keyword2 "and"] prt_asm asms) @
            prt_sect (Pretty.str "subcases:") [] (prt_name o fst) cs))
   end;
 
 in
 
 fun pretty_cases ctxt =
   let
     val cases =
       dest_cases NONE ctxt |> map (fn (name, c as Rule_Cases.Case {fixes, ...}) =>
         (name, (fixes, case_result c ctxt)));
   in
     if null cases then []
     else [Pretty.big_list "cases:" (map pretty_case cases)]
   end;
 
 end;
 
 fun print_cases_proof ctxt0 ctxt =
   let
     fun trim_name x = if Name.is_internal x then Name.clean x else "_";
     val trim_names = map trim_name #> drop_suffix (equal "_");
 
     fun print_case name xs =
       (case trim_names xs of
         [] => print_name ctxt name
       | xs' => enclose "(" ")" (space_implode " " (map (print_name ctxt) (name :: xs'))));
 
     fun is_case x t =
       x = Rule_Cases.case_conclN andalso not (Term.exists_subterm Term.is_Var t);
 
     fun indentation depth = prefix (Symbol.spaces (2 * depth));
 
     fun print_proof depth (name, Rule_Cases.Case {fixes, binds, cases, ...}) =
           let
             val indent = indentation depth;
             val head = indent ("case " ^ print_case name (map (Binding.name_of o #1) fixes));
             val tail =
               if null cases then
                 let val concl =
                   if exists (fn ((x, _), SOME t) => is_case x t | _ => false) binds
                   then Rule_Cases.case_conclN else Auto_Bind.thesisN
                 in indent ("then show ?" ^ concl ^ " sorry") end
               else print_proofs depth cases;
           in head ^ "\n" ^ tail end
     and print_proofs 0 [] = ""
       | print_proofs depth cases =
           let
             val indent = indentation depth;
             val body = map (print_proof (depth + 1)) cases |> separate (indent "next")
           in
             if depth = 0 then body @ [indent "qed"]
             else if length cases = 1 then body
             else indent "{" :: body @ [indent "}"]
           end |> cat_lines;
   in
     (case print_proofs 0 (dest_cases (SOME ctxt0) ctxt) of
       "" => ""
     | s => "Proof outline with cases:\n" ^ Active.sendback_markup_command s)
   end;
 
 
 (* core context *)
 
 val debug = Config.declare_bool ("Proof_Context.debug", \<^here>) (K false);
 val verbose = Config.declare_bool ("Proof_Context.verbose", \<^here>) (K false);
 
 fun pretty_ctxt ctxt =
   if not (Config.get ctxt debug) then []
   else
     let
       val prt_term = Syntax.pretty_term ctxt;
 
       (*structures*)
       val {structs, ...} = Syntax_Trans.get_idents ctxt;
       val prt_structs =
         if null structs then []
         else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 ::
           Pretty.commas (map Pretty.str structs))];
 
       (*fixes*)
       fun prt_fix (x, x') =
         if x = x' then Pretty.str x
         else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')];
       val fixes =
         filter_out ((Name.is_internal orf member (op =) structs) o #1)
           (Variable.dest_fixes ctxt);
       val prt_fixes =
         if null fixes then []
         else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
           Pretty.commas (map prt_fix fixes))];
 
       (*assumptions*)
       val prt_assms =
         (case Assumption.all_prems_of ctxt of
           [] => []
         | prems => [Pretty.big_list "assumptions:" [pretty_fact ctxt ("", prems)]]);
     in prt_structs @ prt_fixes @ prt_assms end;
 
 
 (* main context *)
 
 fun pretty_context ctxt =
   let
     val verbose = Config.get ctxt verbose;
     fun verb f x = if verbose then f (x ()) else [];
 
     val prt_term = Syntax.pretty_term ctxt;
     val prt_typ = Syntax.pretty_typ ctxt;
     val prt_sort = Syntax.pretty_sort ctxt;
 
     (*theory*)
     val pretty_thy = Pretty.block
       [Pretty.str "theory:", Pretty.brk 1, Context.pretty_thy (theory_of ctxt)];
 
     (*defaults*)
     fun prt_atom prt prtT (x, X) = Pretty.block
       [prt x, Pretty.str " ::", Pretty.brk 1, prtT X];
 
     fun prt_var (x, ~1) = prt_term (Syntax.free x)
       | prt_var xi = prt_term (Syntax.var xi);
 
     fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
       | prt_varT xi = prt_typ (TVar (xi, []));
 
     val prt_defT = prt_atom prt_var prt_typ;
     val prt_defS = prt_atom prt_varT prt_sort;
 
     val (types, sorts) = Variable.constraints_of ctxt;
   in
     verb single (K pretty_thy) @
     pretty_ctxt ctxt @
     verb (pretty_abbrevs true false) (K ctxt) @
     verb pretty_term_bindings (K ctxt) @
     verb (pretty_local_facts true) (K ctxt) @
     verb pretty_cases (K ctxt) @
     verb single (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @
     verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts)))
   end;
 
 end;
 
 val show_abbrevs = Proof_Context.show_abbrevs;
diff --git a/src/Pure/Isar/token.ML b/src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML
+++ b/src/Pure/Isar/token.ML
@@ -1,829 +1,830 @@
 (*  Title:      Pure/Isar/token.ML
     Author:     Markus Wenzel, TU Muenchen
 
 Outer token syntax for Isabelle/Isar.
 *)
 
 signature TOKEN =
 sig
   datatype kind =
     (*immediate source*)
     Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
     Float | Space |
     (*delimited content*)
     String | Alt_String | Cartouche |
     Control of Antiquote.control |
     Comment of Comment.kind option |
     (*special content*)
     Error of string | EOF
   val control_kind: kind
   val str_of_kind: kind -> string
   type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
   type T
   type src = T list
   type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring}
   datatype value =
     Source of src |
     Literal of bool * Markup.T |
     Name of name_value * morphism |
     Typ of typ |
     Term of term |
     Fact of string option * thm list |
     Attribute of attribute Morphism.entity |
     Declaration of Morphism.declaration |
     Files of file Exn.result list |
     Output of XML.body option
   val pos_of: T -> Position.T
   val adjust_offsets: (int -> int option) -> T -> T
   val eof: T
   val is_eof: T -> bool
   val not_eof: T -> bool
   val stopper: T Scan.stopper
   val kind_of: T -> kind
   val is_kind: kind -> T -> bool
   val get_control: T -> Antiquote.control option
   val is_command: T -> bool
   val keyword_with: (string -> bool) -> T -> bool
   val is_command_modifier: T -> bool
   val ident_with: (string -> bool) -> T -> bool
   val is_proper: T -> bool
   val is_comment: T -> bool
   val is_informal_comment: T -> bool
   val is_formal_comment: T -> bool
   val is_document_marker: T -> bool
   val is_ignored: T -> bool
   val is_begin_ignore: T -> bool
   val is_end_ignore: T -> bool
   val is_error: T -> bool
   val is_space: T -> bool
   val is_blank: T -> bool
   val is_newline: T -> bool
   val range_of: T list -> Position.range
   val core_range_of: T list -> Position.range
   val content_of: T -> string
   val source_of: T -> string
   val input_of: T -> Input.source
   val inner_syntax_of: T -> string
   val keyword_markup: bool * Markup.T -> string -> Markup.T
   val completion_report: T -> Position.report_text list
   val reports: Keyword.keywords -> T -> Position.report_text list
   val markups: Keyword.keywords -> T -> Markup.T list
   val unparse: T -> string
   val print: T -> string
   val text_of: T -> string * string
   val file_source: file -> Input.source
   val get_files: T -> file Exn.result list
   val put_files: file Exn.result list -> T -> T
   val get_output: T -> XML.body option
   val put_output: XML.body -> T -> T
   val get_value: T -> value option
   val reports_of_value: T -> Position.report list
   val name_value: name_value -> value
   val get_name: T -> name_value option
   val declare_maxidx: T -> Proof.context -> Proof.context
   val map_facts: (string option -> thm list -> thm list) -> T -> T
   val trim_context: T -> T
   val transfer: theory -> T -> T
   val transform: morphism -> T -> T
   val init_assignable: T -> T
   val assign: value option -> T -> T
   val evaluate: ('a -> value) -> (T -> 'a) -> T -> 'a
   val closure: T -> T
   val pretty_value: Proof.context -> T -> Pretty.T
   val name_of_src: src -> string * Position.T
   val args_of_src: src -> T list
   val checked_src: src -> bool
   val check_src: Proof.context -> (Proof.context -> 'a Name_Space.table) -> src -> src * 'a
   val pretty_src: Proof.context -> src -> Pretty.T
   val ident_or_symbolic: string -> bool
   val read_cartouche: Symbol_Pos.T list -> T
   val tokenize: Keyword.keywords -> {strict: bool} -> Symbol_Pos.T list -> T list
   val explode: Keyword.keywords -> Position.T -> string -> T list
   val explode0: Keyword.keywords -> string -> T list
   val print_name: Keyword.keywords -> string -> string
   val print_properties: Keyword.keywords -> Properties.T -> string
   val make: (int * int) * string -> Position.T -> T * Position.T
   val make_string: string * Position.T -> T
   val make_int: int -> T list
   val make_src: string * Position.T -> T list -> src
   type 'a parser = T list -> 'a * T list
   type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
   val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
   val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
 end;
 
 structure Token: TOKEN =
 struct
 
 (** tokens **)
 
 (* token kind *)
 
 datatype kind =
   (*immediate source*)
   Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
   Float | Space |
   (*delimited content*)
   String | Alt_String | Cartouche |
   Control of Antiquote.control |
   Comment of Comment.kind option |
   (*special content*)
   Error of string | EOF;
 
 val control_kind = Control Antiquote.no_control;
 
 fun equiv_kind kind kind' =
   (case (kind, kind') of
     (Control _, Control _) => true
   | (Error _, Error _) => true
   | _ => kind = kind');
 
 val str_of_kind =
  fn Command => "command"
   | Keyword => "keyword"
   | Ident => "identifier"
   | Long_Ident => "long identifier"
   | Sym_Ident => "symbolic identifier"
   | Var => "schematic variable"
   | Type_Ident => "type variable"
   | Type_Var => "schematic type variable"
   | Nat => "natural number"
   | Float => "floating-point number"
   | Space => "white space"
   | String => "quoted string"
   | Alt_String => "back-quoted string"
   | Cartouche => "text cartouche"
   | Control _ => "control cartouche"
   | Comment NONE => "informal comment"
   | Comment (SOME _) => "formal comment"
   | Error _ => "bad input"
   | EOF => "end-of-input";
 
 val immediate_kinds =
   Vector.fromList
     [Command, Keyword, Ident, Long_Ident, Sym_Ident, Var, Type_Ident, Type_Var, Nat, Float, Space];
 
 val delimited_kind =
   (fn String => true
     | Alt_String => true
     | Cartouche => true
     | Control _ => true
     | Comment _ => true
     | _ => false);
 
 
 (* datatype token *)
 
 (*The value slot assigns an (optional) internal value to a token,
   usually as a side-effect of special scanner setup (see also
   args.ML).  Note that an assignable ref designates an intermediate
   state of internalization -- it is NOT meant to persist.*)
 
 type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T};
 
 type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring};
 
 datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot
 
 and slot =
   Slot |
   Value of value option |
   Assignable of value option Unsynchronized.ref
 
 and value =
   Source of T list |
   Literal of bool * Markup.T |
   Name of name_value * morphism |
   Typ of typ |
   Term of term |
   Fact of string option * thm list |  (*optional name for dynamic fact, i.e. fact "variable"*)
   Attribute of attribute Morphism.entity |
   Declaration of Morphism.declaration |
   Files of file Exn.result list |
   Output of XML.body option;
 
 type src = T list;
 
 
 (* position *)
 
 fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
 fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos;
 
 fun adjust_offsets adjust (Token ((x, range), y, z)) =
   Token ((x, apply2 (Position.adjust_offsets adjust) range), y, z);
 
 
 (* stopper *)
 
 fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot);
 val eof = mk_eof Position.none;
 
 fun is_eof (Token (_, (EOF, _), _)) = true
   | is_eof _ = false;
 
 val not_eof = not o is_eof;
 
 val stopper =
   Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
 
 
 (* kind of token *)
 
 fun kind_of (Token (_, (k, _), _)) = k;
 fun is_kind k (Token (_, (k', _), _)) = equiv_kind k k';
 
 fun get_control tok =
   (case kind_of tok of Control control => SOME control | _ => NONE);
 
 val is_command = is_kind Command;
 
 fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
   | keyword_with _ _ = false;
 
 val is_command_modifier = keyword_with (fn x => x = "private" orelse x = "qualified");
 
 fun ident_with pred (Token (_, (Ident, x), _)) = pred x
   | ident_with _ _ = false;
 
 fun is_ignored (Token (_, (Space, _), _)) = true
   | is_ignored (Token (_, (Comment NONE, _), _)) = true
   | is_ignored _ = false;
 
 fun is_proper (Token (_, (Space, _), _)) = false
   | is_proper (Token (_, (Comment _, _), _)) = false
   | is_proper _ = true;
 
 fun is_comment (Token (_, (Comment _, _), _)) = true
   | is_comment _ = false;
 
 fun is_informal_comment (Token (_, (Comment NONE, _), _)) = true
   | is_informal_comment _ = false;
 
 fun is_formal_comment (Token (_, (Comment (SOME _), _), _)) = true
   | is_formal_comment _ = false;
 
 fun is_document_marker (Token (_, (Comment (SOME Comment.Marker), _), _)) = true
   | is_document_marker _ = false;
 
 fun is_begin_ignore (Token (_, (Comment NONE, "<"), _)) = true
   | is_begin_ignore _ = false;
 
 fun is_end_ignore (Token (_, (Comment NONE, ">"), _)) = true
   | is_end_ignore _ = false;
 
 fun is_error (Token (_, (Error _, _), _)) = true
   | is_error _ = false;
 
 
 (* blanks and newlines -- space tokens obey lines *)
 
 fun is_space (Token (_, (Space, _), _)) = true
   | is_space _ = false;
 
 fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x)
   | is_blank _ = false;
 
 fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x
   | is_newline _ = false;
 
 
 (* range of tokens *)
 
 fun range_of (toks as tok :: _) =
       let val pos' = end_pos_of (List.last toks)
       in Position.range (pos_of tok, pos') end
   | range_of [] = Position.no_range;
 
 val core_range_of =
   drop_prefix is_ignored #> drop_suffix is_ignored #> range_of;
 
 
 (* token content *)
 
 fun content_of (Token (_, (_, x), _)) = x;
 fun source_of (Token ((source, _), _, _)) = source;
 
 fun input_of (Token ((source, range), (kind, _), _)) =
   Input.source (delimited_kind kind) source range;
 
 fun inner_syntax_of tok =
   let val x = content_of tok
   in if YXML.detect x then x else Syntax.implode_input (input_of tok) end;
 
 
 (* markup reports *)
 
 local
 
 val token_kind_markup =
  fn Var => (Markup.var, "")
   | Type_Ident => (Markup.tfree, "")
   | Type_Var => (Markup.tvar, "")
   | String => (Markup.string, "")
   | Alt_String => (Markup.alt_string, "")
   | Cartouche => (Markup.cartouche, "")
   | Control _ => (Markup.cartouche, "")
   | Comment _ => (Markup.comment, "")
   | Error msg => (Markup.bad (), msg)
   | _ => (Markup.empty, "");
 
 fun keyword_reports tok = map (fn markup => ((pos_of tok, markup), ""));
 
 fun command_markups keywords x =
   if Keyword.is_theory_end keywords x then [Markup.keyword2 |> Markup.keyword_properties]
   else
     (if Keyword.is_proof_asm keywords x then [Markup.keyword3]
      else if Keyword.is_improper keywords x then [Markup.keyword1, Markup.improper]
      else [Markup.keyword1])
     |> map Markup.command_properties;
 
 in
 
 fun keyword_markup (important, keyword) x =
   if important orelse Symbol.is_ascii_identifier x then keyword else Markup.delimiter;
 
 fun completion_report tok =
   if is_kind Keyword tok
   then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok))
   else [];
 
 fun reports keywords tok =
   if is_command tok then
     keyword_reports tok (command_markups keywords (content_of tok))
   else if is_kind Keyword tok then
     keyword_reports tok
       [keyword_markup (false, Markup.keyword2 |> Markup.keyword_properties) (content_of tok)]
   else
     let
       val pos = pos_of tok;
       val (m, text) = token_kind_markup (kind_of tok);
       val deleted = Symbol_Pos.explode_deleted (source_of tok, pos);
     in ((pos, m), text) :: map (fn p => ((p, Markup.delete), "")) deleted end;
 
 fun markups keywords = map (#2 o #1) o reports keywords;
 
 end;
 
 
 (* unparse *)
 
 fun unparse (Token (_, (kind, x), _)) =
   (case kind of
     String => Symbol_Pos.quote_string_qq x
   | Alt_String => Symbol_Pos.quote_string_bq x
   | Cartouche => cartouche x
   | Control control => Symbol_Pos.content (Antiquote.control_symbols control)
   | Comment NONE => enclose "(*" "*)" x
   | EOF => ""
   | _ => x);
 
 fun print tok = Markup.markups (markups Keyword.empty_keywords tok) (unparse tok);
 
 fun text_of tok =
   let
     val k = str_of_kind (kind_of tok);
     val ms = markups Keyword.empty_keywords tok;
     val s = unparse tok;
   in
     if s = "" then (k, "")
     else if size s < 40 andalso not (exists_string (fn c => c = "\n") s)
     then (k ^ " " ^ Markup.markups ms s, "")
     else (k, Markup.markups ms s)
   end;
 
 
 
 (** associated values **)
 
 (* inlined file content *)
 
 fun file_source (file: file) =
   let
     val text = cat_lines (#lines file);
     val end_pos = Position.symbol_explode text (#pos file);
   in Input.source true text (Position.range (#pos file, end_pos)) end;
 
 fun get_files (Token (_, _, Value (SOME (Files files)))) = files
   | get_files _ = [];
 
 fun put_files [] tok = tok
   | put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files)))
   | put_files _ tok = raise Fail ("Cannot put inlined files here" ^ Position.here (pos_of tok));
 
 
 (* document output *)
 
 fun get_output (Token (_, _, Value (SOME (Output output)))) = output
   | get_output _ = NONE;
 
 fun put_output output (Token (x, y, Slot)) = Token (x, y, Value (SOME (Output (SOME output))))
   | put_output _ tok = raise Fail ("Cannot put document output here" ^ Position.here (pos_of tok));
 
 
 (* access values *)
 
 fun get_value (Token (_, _, Value v)) = v
   | get_value _ = NONE;
 
 fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v)))
   | map_value _ tok = tok;
 
 
 (* reports of value *)
 
 fun get_assignable_value (Token (_, _, Assignable r)) = ! r
   | get_assignable_value (Token (_, _, Value v)) = v
   | get_assignable_value _ = NONE;
 
 fun reports_of_value tok =
   (case get_assignable_value tok of
     SOME (Literal markup) =>
       let
         val pos = pos_of tok;
         val x = content_of tok;
       in
         if Position.is_reported pos then
           map (pair pos) (keyword_markup markup x :: Completion.suppress_abbrevs x)
         else []
       end
   | _ => []);
 
 
 (* name value *)
 
 fun name_value a = Name (a, Morphism.identity);
 
 fun get_name tok =
   (case get_assignable_value tok of
     SOME (Name (a, _)) => SOME a
   | _ => NONE);
 
 
 (* maxidx *)
 
 fun declare_maxidx tok =
   (case get_value tok of
     SOME (Source src) => fold declare_maxidx src
   | SOME (Typ T) => Variable.declare_maxidx (Term.maxidx_of_typ T)
   | SOME (Term t) => Variable.declare_maxidx (Term.maxidx_of_term t)
   | SOME (Fact (_, ths)) => fold (Variable.declare_maxidx o Thm.maxidx_of) ths
   | SOME (Attribute _) => I  (* FIXME !? *)
   | SOME (Declaration decl) =>
       (fn ctxt =>
         let val ctxt' = Context.proof_map (Morphism.form decl) ctxt
         in Variable.declare_maxidx (Variable.maxidx_of ctxt') ctxt end)
   | _ => I);
 
 
 (* fact values *)
 
 fun map_facts f =
   map_value (fn v =>
     (case v of
       Source src => Source (map (map_facts f) src)
     | Fact (a, ths) => Fact (a, f a ths)
     | _ => v));
 
 
 (* implicit context *)
 
 local
 
 fun context thm_context morphism_context attribute_context declaration_context =
   let
     fun token_context tok = map_value
       (fn Source src => Source (map token_context src)
         | Fact (a, ths) => Fact (a, map thm_context ths)
         | Name (a, phi) => Name (a, morphism_context phi)
         | Attribute a => Attribute (attribute_context a)
         | Declaration a => Declaration (declaration_context a)
         | v => v) tok;
   in token_context end;
 
 in
 
 val trim_context =
   context Thm.trim_context Morphism.reset_context
     Morphism.entity_reset_context Morphism.entity_reset_context;
 
 fun transfer thy =
   context (Thm.transfer thy) (Morphism.set_context thy)
     (Morphism.entity_set_context thy) (Morphism.entity_set_context thy);
 
 end;
 
 
 (* transform *)
 
 fun transform phi =
   map_value (fn v =>
     (case v of
       Source src => Source (map (transform phi) src)
     | Literal _ => v
     | Name (a, psi) => Name (a, psi $> phi)
     | Typ T => Typ (Morphism.typ phi T)
     | Term t => Term (Morphism.term phi t)
     | Fact (a, ths) => Fact (a, Morphism.fact phi ths)
     | Attribute att => Attribute (Morphism.transform phi att)
     | Declaration decl => Declaration (Morphism.transform phi decl)
     | Files _ => v
     | Output _ => v));
 
 
 (* static binding *)
 
 (*1st stage: initialize assignable slots*)
 fun init_assignable tok =
   (case tok of
     Token (x, y, Slot) => Token (x, y, Assignable (Unsynchronized.ref NONE))
   | Token (_, _, Value _) => tok
   | Token (_, _, Assignable r) => (r := NONE; tok));
 
 (*2nd stage: assign values as side-effect of scanning*)
 fun assign v tok =
   (case tok of
     Token (x, y, Slot) => Token (x, y, Value v)
   | Token (_, _, Value _) => tok
   | Token (_, _, Assignable r) => (r := v; tok));
 
 fun evaluate mk eval arg =
   let val x = eval arg in (assign (SOME (mk x)) arg; x) end;
 
 (*3rd stage: static closure of final values*)
 fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
   | closure tok = tok;
 
 
 (* pretty *)
 
 fun pretty_value ctxt tok =
   (case get_value tok of
     SOME (Literal markup) =>
       let val x = content_of tok
       in Pretty.mark_str (keyword_markup markup x, x) end
   | SOME (Name ({print, ...}, _)) => Pretty.quote (Pretty.mark_str (print ctxt))
   | SOME (Typ T) => Syntax.pretty_typ ctxt T
   | SOME (Term t) => Syntax.pretty_term ctxt t
   | SOME (Fact (_, ths)) =>
       Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.cartouche o Thm.pretty_thm ctxt) ths))
   | _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok));
 
 
 (* src *)
 
 fun dest_src ([]: src) = raise Fail "Empty token source"
   | dest_src (head :: args) = (head, args);
 
 fun name_of_src src =
   let
     val head = #1 (dest_src src);
     val name =
       (case get_name head of
         SOME {name, ...} => name
       | NONE => content_of head);
   in (name, pos_of head) end;
 
 val args_of_src = #2 o dest_src;
 
 fun pretty_src ctxt src =
   let
     val (head, args) = dest_src src;
     val prt_name =
       (case get_name head of
         SOME {print, ...} => Pretty.mark_str (print ctxt)
       | NONE => Pretty.str (content_of head));
   in Pretty.block (Pretty.breaks (Pretty.quote prt_name :: map (pretty_value ctxt) args)) end;
 
 fun checked_src (head :: _) = is_some (get_name head)
   | checked_src [] = true;
 
 fun check_src ctxt get_table src =
   let
     val (head, args) = dest_src src;
     val table = get_table ctxt;
   in
     (case get_name head of
       SOME {name, ...} => (src, Name_Space.get table name)
     | NONE =>
         let
           val pos = pos_of head;
           val (name, x) = Name_Space.check (Context.Proof ctxt) table (content_of head, pos);
           val _ = Context_Position.report ctxt pos Markup.operator;
           val kind = Name_Space.kind_of (Name_Space.space_of_table table);
           fun print ctxt' =
             Name_Space.markup_extern ctxt' (Name_Space.space_of_table (get_table ctxt')) name;
           val value = name_value {name = name, kind = kind, print = print};
           val head' = closure (assign (SOME value) head);
         in (head' :: args, x) end)
   end;
 
 
 
 (** scanners **)
 
 open Basic_Symbol_Pos;
 
 val err_prefix = "Outer lexical error: ";
 
 fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
 
 
 (* scan symbolic idents *)
 
 val scan_symid =
   Scan.many1 (Symbol.is_symbolic_char o Symbol_Pos.symbol) ||
   Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> single;
 
 fun is_symid str =
   (case try Symbol.explode str of
     SOME [s] => Symbol.is_symbolic s orelse Symbol.is_symbolic_char s
   | SOME ss => forall Symbol.is_symbolic_char ss
   | _ => false);
 
 fun ident_or_symbolic "begin" = false
   | ident_or_symbolic ":" = true
   | ident_or_symbolic "::" = true
   | ident_or_symbolic s = Symbol_Pos.is_identifier s orelse is_symid s;
 
 
 (* scan cartouche *)
 
 val scan_cartouche =
   Symbol_Pos.scan_pos --
     ((Symbol_Pos.scan_cartouche err_prefix >> Symbol_Pos.cartouche_content) -- Symbol_Pos.scan_pos);
 
 
 (* scan space *)
 
 fun space_symbol (s, _) = Symbol.is_blank s andalso s <> "\n";
 
 val scan_space =
   Scan.many1 space_symbol @@@ Scan.optional ($$$ "\n") [] ||
   Scan.many space_symbol @@@ $$$ "\n";
 
 
 (* scan comment *)
 
 val scan_comment =
   Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body err_prefix -- Symbol_Pos.scan_pos);
 
 
 
 (** token sources **)
 
 local
 
 fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
 
 fun token k ss =
   Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot);
 
 fun token_range k (pos1, (ss, pos2)) =
   Token (Symbol_Pos.implode_range (pos1, pos2) ss, (k, Symbol_Pos.content ss), Slot);
 
 fun scan_token keywords = !!! "bad input"
   (Symbol_Pos.scan_string_qq err_prefix >> token_range String ||
     Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String ||
     scan_comment >> token_range (Comment NONE) ||
     Comment.scan_outer >> (fn (k, ss) => token (Comment (SOME k)) ss) ||
     scan_cartouche >> token_range Cartouche ||
     Antiquote.scan_control err_prefix >> (fn control =>
       token (Control control) (Antiquote.control_symbols control)) ||
     scan_space >> token Space ||
     (Scan.max token_leq
       (Scan.max token_leq
         (Scan.literal (Keyword.major_keywords keywords) >> pair Command)
         (Scan.literal (Keyword.minor_keywords keywords) >> pair Keyword))
       (Lexicon.scan_longid >> pair Long_Ident ||
         Lexicon.scan_id >> pair Ident ||
         Lexicon.scan_var >> pair Var ||
         Lexicon.scan_tid >> pair Type_Ident ||
         Lexicon.scan_tvar >> pair Type_Var ||
         Symbol_Pos.scan_float >> pair Float ||
         Symbol_Pos.scan_nat >> pair Nat ||
         scan_symid >> pair Sym_Ident) >> uncurry token));
 
 fun recover msg =
   (Symbol_Pos.recover_string_qq ||
     Symbol_Pos.recover_string_bq ||
     Symbol_Pos.recover_cartouche ||
     Symbol_Pos.recover_comment ||
     Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single)
   >> (single o token (Error msg));
 
 in
 
 fun make_source keywords {strict} =
   let
     val scan_strict = Scan.bulk (scan_token keywords);
     val scan = if strict then scan_strict else Scan.recover scan_strict recover;
   in Source.source Symbol_Pos.stopper scan end;
 
 fun read_cartouche syms =
   (case Scan.read Symbol_Pos.stopper (scan_cartouche >> token_range Cartouche) syms of
     SOME tok => tok
   | NONE => error ("Single cartouche expected" ^ Position.here (#1 (Symbol_Pos.range syms))));
 
 end;
 
 
 (* explode *)
 
 fun tokenize keywords strict syms =
   Source.of_list syms |> make_source keywords strict |> Source.exhaust;
 
 fun explode keywords pos text =
   Symbol_Pos.explode (text, pos) |> tokenize keywords {strict = false};
 
 fun explode0 keywords = explode keywords Position.none;
 
 
 (* print names in parsable form *)
 
 fun print_name keywords name =
   ((case explode keywords Position.none name of
     [tok] => not (member (op =) [Ident, Long_Ident, Sym_Ident, Nat] (kind_of tok))
   | _ => true) ? Symbol_Pos.quote_string_qq) name;
 
 fun print_properties keywords =
   map (apply2 (print_name keywords) #> (fn (a, b) => a ^ " = " ^ b)) #> commas #> enclose "[" "]";
 
 
 (* make *)
 
 fun make ((k, n), s) pos =
   let
     val pos' = Position.shift_offsets {remove_id = false} n pos;
     val range = Position.range (pos, pos');
     val tok =
       if 0 <= k andalso k < Vector.length immediate_kinds then
         Token ((s, range), (Vector.nth immediate_kinds k, s), Slot)
       else
         (case explode Keyword.empty_keywords pos s of
           [tok] => tok
         | _ => Token ((s, range), (Error (err_prefix ^ "exactly one token expected"), s), Slot))
   in (tok, pos') end;
 
 fun make_string (s, pos) =
   let
     val Token ((x, _), y, z) = #1 (make ((~1, 0), Symbol_Pos.quote_string_qq s) Position.none);
     val pos' = Position.no_range_position pos;
   in Token ((x, (pos', pos')), y, z) end;
 
 val make_int = explode Keyword.empty_keywords Position.none o signed_string_of_int;
 
 fun make_src a args = make_string a :: args;
 
 
 
 (** parsers **)
 
 type 'a parser = T list -> 'a * T list;
 type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list);
 
 
 (* wrapped syntax *)
 
-fun syntax_generic scan src context =
+fun syntax_generic scan src0 context =
   let
+    val src = map (transfer (Context.theory_of context)) src0;
     val (name, pos) = name_of_src src;
     val old_reports = maps reports_of_value src;
     val args1 = map init_assignable (args_of_src src);
     fun reported_text () =
       if Context_Position.reports_enabled_generic context then
         let val new_reports = maps (reports_of_value o closure) args1 in
           if old_reports <> new_reports then
             map (fn (p, m) => Position.reported_text p m "") new_reports
           else []
         end
       else [];
   in
     (case Scan.error (Scan.finite' stopper (Scan.option scan)) (context, args1) of
       (SOME x, (context', [])) =>
         let val _ = Output.report (reported_text ())
         in (x, context') end
     | (_, (context', args2)) =>
         let
           val print_name =
             (case get_name (hd src) of
               NONE => quote name
             | SOME {kind, print, ...} =>
                 let
                   val ctxt' = Context.proof_of context';
                   val (markup, xname) = print ctxt';
                 in plain_words kind ^ " " ^ quote (Markup.markup markup xname) end);
           val print_args =
             if null args2 then "" else ":\n  " ^ space_implode " " (map print args2);
         in
           error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^
             Markup.markup_report (implode (reported_text ())))
         end)
   end;
 
 fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof;
 
 end;
 
 type 'a parser = 'a Token.parser;
 type 'a context_parser = 'a Token.context_parser;
diff --git a/src/Pure/assumption.ML b/src/Pure/assumption.ML
--- a/src/Pure/assumption.ML
+++ b/src/Pure/assumption.ML
@@ -1,149 +1,156 @@
 (*  Title:      Pure/assumption.ML
     Author:     Makarius
 
 Context assumptions, parameterized by export rules.
 *)
 
 signature ASSUMPTION =
 sig
   type export = bool -> cterm list -> (thm -> thm) * (term -> term)
   val assume_export: export
   val presume_export: export
   val assume: Proof.context -> cterm -> thm
   val assume_hyps: cterm -> Proof.context -> thm * Proof.context
   val all_assms_of: Proof.context -> cterm list
   val all_prems_of: Proof.context -> thm list
   val local_assms_of: Proof.context -> Proof.context -> cterm list
   val local_prems_of: Proof.context -> Proof.context -> thm list
   val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context
   val add_assumes: cterm list -> Proof.context -> thm list * Proof.context
+  val export_term: Proof.context -> Proof.context -> term -> term
   val export: bool -> Proof.context -> Proof.context -> thm -> thm
-  val export_term: Proof.context -> Proof.context -> term -> term
   val export_morphism: Proof.context -> Proof.context -> morphism
 end;
 
 structure Assumption: ASSUMPTION =
 struct
 
 (** basic rules **)
 
 type export = bool -> cterm list -> (thm -> thm) * (term -> term);
 
 (*
     [A]
      :
      B
   --------
   #A \<Longrightarrow> B
 *)
 fun assume_export is_goal asms =
   (if is_goal then Drule.implies_intr_protected asms else Drule.implies_intr_list asms, fn t => t);
 
 (*
     [A]
      :
      B
   -------
   A \<Longrightarrow> B
 *)
 fun presume_export _ = assume_export false;
 
 
 fun assume ctxt = Raw_Simplifier.norm_hhf ctxt o Thm.assume;
 
 fun assume_hyps ct ctxt =
   let val (th, ctxt') = Thm.assume_hyps ct ctxt
   in (Raw_Simplifier.norm_hhf ctxt' th, ctxt') end;
 
 
 
 (** local context data **)
 
 datatype data = Data of
  {assms: (export * cterm list) list,    (*assumes: A \<Longrightarrow> _*)
   prems: thm list};                     (*prems: A |- norm_hhf A*)
 
 fun make_data (assms, prems) = Data {assms = assms, prems = prems};
 val empty_data = make_data ([], []);
 
 structure Data = Proof_Data
 (
   type T = data;
   fun init _ = empty_data;
 );
 
 fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
 
 
 (* all assumptions *)
 
 val all_assumptions_of = #assms o rep_data;
 val all_assms_of = maps #2 o all_assumptions_of;
 val all_prems_of = #prems o rep_data;
 
 
 (* local assumptions *)
 
 local
 
 fun drop_prefix eq (args as (x :: xs, y :: ys)) =
       if eq (x, y) then drop_prefix eq (xs, ys) else args
   | drop_prefix _ args = args;
 
 fun check_result ctxt kind term_of res =
   (case res of
     ([], rest) => rest
   | (bad :: _, _) =>
       raise Fail ("Outer context disagrees on " ^ kind ^ ": " ^
         Syntax.string_of_term ctxt (term_of bad)));
 
 in
 
 fun local_assumptions_of inner outer =
   drop_prefix (eq_snd (eq_list Thm.aconvc)) (apply2 all_assumptions_of (outer, inner))
   |>> maps #2
   |> check_result outer "assumption" Thm.term_of;
 
 val local_assms_of = maps #2 oo local_assumptions_of;
 
 fun local_prems_of inner outer =
   drop_prefix Thm.eq_thm_prop (apply2 all_prems_of (outer, inner))
   |> check_result outer "premise" Thm.prop_of;
 
 end;
 
 
 (* add assumptions *)
 
 fun add_assms export new_asms ctxt =
   let val (new_prems, ctxt') = fold_map assume_hyps new_asms ctxt in
     ctxt'
     |> map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems))
     |> pair new_prems
   end;
 
 val add_assumes = add_assms assume_export;
 
 
 (* export *)
 
-fun export is_goal inner outer =
-  Raw_Simplifier.norm_hhf_protect_without_context #>
-  fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
-  Raw_Simplifier.norm_hhf_protect_without_context;
-
 fun export_term inner outer =
   fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
 
+fun export_thm is_goal inner outer =
+  fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer);
+
+fun export is_goal inner outer =
+  Raw_Simplifier.norm_hhf_protect inner #>
+  export_thm is_goal inner outer #>
+  Raw_Simplifier.norm_hhf_protect outer;
+
 fun export_morphism inner outer =
   let
-    val thm = export false inner outer;
+    val export0 = export_thm false inner outer;
+    fun thm thy =
+      let val norm = norm_hhf_protect (Proof_Context.init_global thy)
+      in norm #> export0 #> norm end;
     val term = export_term inner outer;
     val typ = Logic.type_map term;
   in
     Morphism.morphism "Assumption.export"
-      {binding = [], typ = [K typ], term = [K term], fact = [K (map thm)]}
+      {binding = [], typ = [K typ], term = [K term], fact = [map o thm o Morphism.the_theory]}
+    |> Morphism.set_context (Proof_Context.theory_of inner)
   end;
 
 end;
diff --git a/src/Pure/goal.ML b/src/Pure/goal.ML
--- a/src/Pure/goal.ML
+++ b/src/Pure/goal.ML
@@ -1,340 +1,336 @@
 (*  Title:      Pure/goal.ML
     Author:     Makarius
 
 Goals in tactical theorem proving, with support for forked proofs.
 *)
 
 signature BASIC_GOAL =
 sig
   val quick_and_dirty: bool Config.T
   val SELECT_GOAL: tactic -> int -> tactic
   val PREFER_GOAL: tactic -> int -> tactic
   val CONJUNCTS: tactic -> int -> tactic
   val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
 end;
 
 signature GOAL =
 sig
   include BASIC_GOAL
   val init: cterm -> thm
   val protect: int -> thm -> thm
   val conclude: thm -> thm
   val check_finished: Proof.context -> thm -> thm
   val finish: Proof.context -> thm -> thm
   val norm_result: Proof.context -> thm -> thm
-  val norm_result_without_context: thm -> thm
   val skip_proofs_enabled: unit -> bool
   val future_result: Proof.context -> thm future -> term -> thm
   val prove_internal: Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm
   val prove_common: Proof.context -> int option -> string list -> term list -> term list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm list
   val prove_future: Proof.context -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
   val prove: Proof.context -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
   val prove_global_future: theory -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
   val prove_global: theory -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
   val prove_sorry: Proof.context -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
   val prove_sorry_global: theory -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
   val restrict: int -> int -> thm -> thm
   val unrestrict: int -> thm -> thm
   val conjunction_tac: int -> tactic
   val precise_conjunction_tac: int -> int -> tactic
   val recover_conjunction_tac: tactic
   val norm_hhf_tac: Proof.context -> int -> tactic
   val assume_rule_tac: Proof.context -> int -> tactic
 end;
 
 structure Goal: GOAL =
 struct
 
 (** goals **)
 
 (*
   -------- (init)
   C \<Longrightarrow> #C
 *)
 fun init C = Thm.instantiate (TVars.empty, Vars.make1 ((("A", 0), propT), C)) Drule.protectI;
 
 (*
   A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> C
   ------------------------ (protect n)
   A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> #C
 *)
 fun protect n th = Drule.comp_no_flatten (th, n) 1 Drule.protectI;
 
 (*
   A \<Longrightarrow> ... \<Longrightarrow> #C
   ---------------- (conclude)
   A \<Longrightarrow> ... \<Longrightarrow> C
 *)
 fun conclude th = Drule.comp_no_flatten (th, Thm.nprems_of th) 1 Drule.protectD;
 
 (*
   #C
   --- (finish)
    C
 *)
 fun check_finished ctxt th =
   if Thm.no_prems th then th
   else raise THM ("Proof failed.\n" ^ Goal_Display.string_of_goal ctxt th, 0, [th]);
 
 fun finish ctxt = check_finished ctxt #> conclude;
 
 
 
 (** results **)
 
 (* normal form *)
 
 fun norm_result ctxt =
   Drule.flexflex_unique (SOME ctxt)
   #> Raw_Simplifier.norm_hhf_protect ctxt
   #> Thm.strip_shyps
   #> Drule.zero_var_indexes;
 
-fun norm_result_without_context th =
-  norm_result (Proof_Context.init_global (Thm.theory_of_thm th)) th;
-
 
 (* scheduling parameters *)
 
 fun skip_proofs_enabled () =
   let val skip = Options.default_bool "skip_proofs" in
     if Proofterm.proofs_enabled () andalso skip then
       (warning "Proof terms enabled -- cannot skip proofs"; false)
     else skip
   end;
 
 
 (* future_result *)
 
 fun future_result ctxt result prop =
   let
     val assms = Assumption.all_assms_of ctxt;
     val As = map Thm.term_of assms;
 
     val frees = Frees.build (fold Frees.add_frees (prop :: As));
     val xs = Frees.fold_rev (cons o Thm.cterm_of ctxt o Free o #1) frees [];
 
     val tfrees = TFrees.build (fold TFrees.add_tfrees (prop :: As));
     val Ts = Names.build (TFrees.fold (Names.add_set o #1 o #1) tfrees);
     val instT =
       TVars.build (tfrees |> TFrees.fold (fn ((a, S), _) =>
         TVars.add (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))));
 
     val global_prop =
       Logic.list_implies (As, prop)
       |> Frees.fold_rev (Logic.all o Free o #1) frees
       |> Logic.varify_types_global
       |> Thm.cterm_of ctxt
       |> Thm.weaken_sorts' ctxt;
     val global_result = result |> Future.map
       (Drule.flexflex_unique (SOME ctxt) #>
         Drule.implies_intr_list assms #>
         Drule.forall_intr_list xs #>
         Thm.adjust_maxidx_thm ~1 #>
         Thm.generalize (Ts, Names.empty) 0 #>
         Thm.strip_shyps #>
         Thm.solve_constraints);
     val local_result =
       Thm.future global_result global_prop
       |> Thm.close_derivation \<^here>
       |> Thm.instantiate (instT, Vars.empty)
       |> Drule.forall_elim_list xs
       |> fold (Thm.elim_implies o Thm.assume) assms
       |> Thm.solve_constraints;
   in local_result end;
 
 
 
 (** tactical theorem proving **)
 
 (* prove_internal -- minimal checks, no normalization of result! *)
 
 fun prove_internal ctxt casms cprop tac =
   (case SINGLE (tac (map (Assumption.assume ctxt) casms)) (init cprop) of
     SOME th => Drule.implies_intr_list casms (finish ctxt th)
   | NONE => error "Tactic failed");
 
 
 (* prove variations *)
 
 fun prove_common ctxt fork_pri xs asms props tac =
   let
     val thy = Proof_Context.theory_of ctxt;
 
     val schematic = exists Term.is_schematic props;
     val immediate = is_none fork_pri;
     val future = Future.proofs_enabled 1 andalso not (Proofterm.proofs_enabled ());
     val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled ();
 
     val pos = Position.thread_data ();
     fun err msg =
       cat_error msg
         ("The error(s) above occurred for the goal statement" ^ Position.here pos ^ ":\n" ^
           Syntax.string_of_term ctxt (Logic.list_implies (asms, Logic.mk_conjunction_list props)));
 
     fun cert_safe t = Thm.cterm_of ctxt (Envir.beta_norm (Term.no_dummy_patterns t))
       handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
     val casms = map cert_safe asms;
     val cprops = map cert_safe props;
 
     val (prems, ctxt') = ctxt
       |> Variable.add_fixes_direct xs
       |> fold Variable.declare_term (asms @ props)
       |> Assumption.add_assumes casms
       ||> Variable.set_body true;
 
     val stmt = Thm.weaken_sorts' ctxt' (Conjunction.mk_conjunction_balanced cprops);
 
     fun tac' args st =
       if skip then ALLGOALS (Skip_Proof.cheat_tac ctxt) st before Skip_Proof.report ctxt
       else tac args st;
     fun result () =
       (case SINGLE (tac' {prems = prems, context = ctxt'}) (init stmt) of
         NONE => err "Tactic failed"
       | SOME st =>
           let
             val _ =
               Context.subthy_id (Thm.theory_id st, Context.theory_id thy) orelse
                 err "Bad background theory of goal state";
             val res =
               (finish ctxt' st
                 |> Drule.flexflex_unique (SOME ctxt')
                 |> Thm.check_shyps ctxt'
                 |> Thm.check_hyps (Context.Proof ctxt'))
               handle THM (msg, _, _) => err msg | ERROR msg => err msg;
           in
             if is_none (Unify.matcher (Context.Proof ctxt') [Thm.term_of stmt] [Thm.prop_of res])
             then err ("Proved a different theorem: " ^ Syntax.string_of_term ctxt' (Thm.prop_of res))
             else res
           end);
     val res =
       if immediate orelse schematic orelse not future orelse skip then result ()
       else
         future_result ctxt'
           (Execution.fork {name = "Goal.prove", pos = Position.thread_data (), pri = the fork_pri}
             result)
           (Thm.term_of stmt);
   in
     res
     |> Thm.close_derivation \<^here>
     |> Conjunction.elim_balanced (length props)
     |> map (Assumption.export false ctxt' ctxt)
     |> Variable.export ctxt' ctxt
     |> map Drule.zero_var_indexes
   end;
 
 fun prove_future_pri ctxt pri xs asms prop tac =
   hd (prove_common ctxt (SOME pri) xs asms [prop] tac);
 
 fun prove_future ctxt = prove_future_pri ctxt ~1;
 
 fun prove ctxt xs asms prop tac = hd (prove_common ctxt NONE xs asms [prop] tac);
 
 fun prove_global_future thy xs asms prop tac =
   Drule.export_without_context (prove_future (Proof_Context.init_global thy) xs asms prop tac);
 
 fun prove_global thy xs asms prop tac =
   Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);
 
 
 (* skip proofs *)
 
 val quick_and_dirty = Config.declare_option_bool ("quick_and_dirty", \<^here>);
 
 fun prove_sorry ctxt xs asms prop tac =
   if Config.get ctxt quick_and_dirty then
     prove ctxt xs asms prop (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt))
   else (if Future.proofs_enabled 1 then prove_future_pri ctxt ~2 else prove ctxt) xs asms prop tac;
 
 fun prove_sorry_global thy xs asms prop tac =
   Drule.export_without_context
     (prove_sorry (Proof_Context.init_global thy) xs asms prop tac);
 
 
 
 (** goal structure **)
 
 (* rearrange subgoals *)
 
 fun restrict i n st =
   if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st
   then raise THM ("Goal.restrict", i, [st])
   else rotate_prems (i - 1) st |> protect n;
 
 fun unrestrict i = conclude #> rotate_prems (1 - i);
 
 (*with structural marker*)
 fun SELECT_GOAL tac i st =
   if Thm.nprems_of st = 1 andalso i = 1 then tac st
   else (PRIMITIVE (restrict i 1) THEN tac THEN PRIMITIVE (unrestrict i)) st;
 
 (*without structural marker*)
 fun PREFER_GOAL tac i st =
   if i < 1 orelse i > Thm.nprems_of st then Seq.empty
   else (PRIMITIVE (rotate_prems (i - 1)) THEN tac THEN PRIMITIVE (rotate_prems (1 - i))) st;
 
 
 (* multiple goals *)
 
 fun precise_conjunction_tac 0 i = eq_assume_tac i
   | precise_conjunction_tac 1 i = SUBGOAL (K all_tac) i
   | precise_conjunction_tac n i = PRIMITIVE (Drule.with_subgoal i (Conjunction.curry_balanced n));
 
 val adhoc_conjunction_tac = REPEAT_ALL_NEW
   (SUBGOAL (fn (goal, i) =>
     if can Logic.dest_conjunction goal then resolve0_tac [Conjunction.conjunctionI] i
     else no_tac));
 
 val conjunction_tac = SUBGOAL (fn (goal, i) =>
   precise_conjunction_tac (length (Logic.dest_conjunctions goal)) i ORELSE
   TRY (adhoc_conjunction_tac i));
 
 val recover_conjunction_tac = PRIMITIVE (fn th =>
   Conjunction.uncurry_balanced (Thm.nprems_of th) th);
 
 fun PRECISE_CONJUNCTS n tac =
   SELECT_GOAL (precise_conjunction_tac n 1
     THEN tac
     THEN recover_conjunction_tac);
 
 fun CONJUNCTS tac =
   SELECT_GOAL (conjunction_tac 1
     THEN tac
     THEN recover_conjunction_tac);
 
 
 (* hhf normal form *)
 
 fun norm_hhf_tac ctxt =
   resolve_tac ctxt [Drule.asm_rl]  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
   THEN' SUBGOAL (fn (t, i) =>
     if Drule.is_norm_hhf {protect = false} t then all_tac
     else rewrite_goal_tac ctxt Drule.norm_hhf_eqs i);
 
 
 (* non-atomic goal assumptions *)
 
 fun non_atomic (Const ("Pure.imp", _) $ _ $ _) = true
   | non_atomic (Const ("Pure.all", _) $ _) = true
   | non_atomic _ = false;
 
 fun assume_rule_tac ctxt = norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) =>
   let
     val ((_, goal'), ctxt') = Variable.focus_cterm NONE goal ctxt;
     val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
     val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
     val tacs = Rs |> map (fn R =>
       eresolve_tac ctxt [Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)] THEN_ALL_NEW assume_tac ctxt);
   in fold_rev (curry op APPEND') tacs (K no_tac) i end);
 
 end;
 
 structure Basic_Goal: BASIC_GOAL = Goal;
 open Basic_Goal;
diff --git a/src/Pure/raw_simplifier.ML b/src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML
+++ b/src/Pure/raw_simplifier.ML
@@ -1,1460 +1,1456 @@
 (*  Title:      Pure/raw_simplifier.ML
     Author:     Tobias Nipkow and Stefan Berghofer, TU Muenchen
 
 Higher-order Simplification.
 *)
 
 infix 4
   addsimps delsimps addsimprocs delsimprocs
   setloop addloop delloop
   setSSolver addSSolver setSolver addSolver;
 
 signature BASIC_RAW_SIMPLIFIER =
 sig
   val simp_depth_limit: int Config.T
   val simp_trace_depth_limit: int Config.T
   val simp_debug: bool Config.T
   val simp_trace: bool Config.T
   type cong_name = bool * string
   type rrule
   val mk_rrules: Proof.context -> thm list -> rrule list
   val eq_rrule: rrule * rrule -> bool
   type proc
   type solver
   val mk_solver: string -> (Proof.context -> int -> tactic) -> solver
   type simpset
   val empty_ss: simpset
   val merge_ss: simpset * simpset -> simpset
   val dest_ss: simpset ->
    {simps: (string * thm) list,
     procs: (string * term list) list,
     congs: (cong_name * thm) list,
     weak_congs: cong_name list,
     loopers: string list,
     unsafe_solvers: string list,
     safe_solvers: string list}
   type simproc
   val eq_simproc: simproc * simproc -> bool
   val cert_simproc: theory -> string ->
     {lhss: term list, proc: (Proof.context -> cterm -> thm option) Morphism.entity} -> simproc
   val transform_simproc: morphism -> simproc -> simproc
   val simpset_of: Proof.context -> simpset
   val put_simpset: simpset -> Proof.context -> Proof.context
   val simpset_map: Proof.context -> (Proof.context -> Proof.context) -> simpset -> simpset
   val map_theory_simpset: (Proof.context -> Proof.context) -> theory -> theory
   val empty_simpset: Proof.context -> Proof.context
   val clear_simpset: Proof.context -> Proof.context
   val addsimps: Proof.context * thm list -> Proof.context
   val delsimps: Proof.context * thm list -> Proof.context
   val addsimprocs: Proof.context * simproc list -> Proof.context
   val delsimprocs: Proof.context * simproc list -> Proof.context
   val setloop: Proof.context * (Proof.context -> int -> tactic) -> Proof.context
   val addloop: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context
   val delloop: Proof.context * string -> Proof.context
   val setSSolver: Proof.context * solver -> Proof.context
   val addSSolver: Proof.context * solver -> Proof.context
   val setSolver: Proof.context * solver -> Proof.context
   val addSolver: Proof.context * solver -> Proof.context
 
   val rewrite_rule: Proof.context -> thm list -> thm -> thm
   val rewrite_goals_rule: Proof.context -> thm list -> thm -> thm
   val rewrite_goals_tac: Proof.context -> thm list -> tactic
   val rewrite_goal_tac: Proof.context -> thm list -> int -> tactic
   val prune_params_tac: Proof.context -> tactic
   val fold_rule: Proof.context -> thm list -> thm -> thm
   val fold_goals_tac: Proof.context -> thm list -> tactic
   val norm_hhf: Proof.context -> thm -> thm
   val norm_hhf_protect: Proof.context -> thm -> thm
-  val norm_hhf_protect_without_context: thm -> thm
 end;
 
 signature RAW_SIMPLIFIER =
 sig
   include BASIC_RAW_SIMPLIFIER
   exception SIMPLIFIER of string * thm list
   type trace_ops
   val set_trace_ops: trace_ops -> theory -> theory
   val subgoal_tac: Proof.context -> int -> tactic
   val loop_tac: Proof.context -> int -> tactic
   val solvers: Proof.context -> solver list * solver list
   val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic
   val prems_of: Proof.context -> thm list
   val add_simp: thm -> Proof.context -> Proof.context
   val del_simp: thm -> Proof.context -> Proof.context
   val flip_simp: thm -> Proof.context -> Proof.context
   val init_simpset: thm list -> Proof.context -> Proof.context
   val add_eqcong: thm -> Proof.context -> Proof.context
   val del_eqcong: thm -> Proof.context -> Proof.context
   val add_cong: thm -> Proof.context -> Proof.context
   val del_cong: thm -> Proof.context -> Proof.context
   val mksimps: Proof.context -> thm -> thm list
   val set_mksimps: (Proof.context -> thm -> thm list) -> Proof.context -> Proof.context
   val set_mkcong: (Proof.context -> thm -> thm) -> Proof.context -> Proof.context
   val set_mksym: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context
   val set_mkeqTrue: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context
   val set_term_ord: term ord -> Proof.context -> Proof.context
   val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
   val solver: Proof.context -> solver -> int -> tactic
   val default_mk_sym: Proof.context -> thm -> thm option
   val add_prems: thm list -> Proof.context -> Proof.context
   val set_reorient: (Proof.context -> term list -> term -> term -> bool) ->
     Proof.context -> Proof.context
   val set_solvers: solver list -> Proof.context -> Proof.context
   val rewrite_cterm: bool * bool * bool ->
     (Proof.context -> thm -> thm option) -> Proof.context -> conv
   val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term
   val rewrite_thm: bool * bool * bool ->
     (Proof.context -> thm -> thm option) -> Proof.context -> thm -> thm
   val generic_rewrite_goal_tac: bool * bool * bool ->
     (Proof.context -> tactic) -> Proof.context -> int -> tactic
   val rewrite: Proof.context -> bool -> thm list -> conv
 end;
 
 structure Raw_Simplifier: RAW_SIMPLIFIER =
 struct
 
 (** datatype simpset **)
 
 (* congruence rules *)
 
 type cong_name = bool * string;
 
 fun cong_name (Const (a, _)) = SOME (true, a)
   | cong_name (Free (a, _)) = SOME (false, a)
   | cong_name _ = NONE;
 
 structure Congtab = Table(type key = cong_name val ord = prod_ord bool_ord fast_string_ord);
 
 
 (* rewrite rules *)
 
 type rrule =
  {thm: thm,         (*the rewrite rule*)
   name: string,     (*name of theorem from which rewrite rule was extracted*)
   lhs: term,        (*the left-hand side*)
   elhs: cterm,      (*the eta-contracted lhs*)
   extra: bool,      (*extra variables outside of elhs*)
   fo: bool,         (*use first-order matching*)
   perm: bool};      (*the rewrite rule is permutative*)
 
 fun trim_context_rrule ({thm, name, lhs, elhs, extra, fo, perm}: rrule) =
   {thm = Thm.trim_context thm, name = name, lhs = lhs, elhs = Thm.trim_context_cterm elhs,
     extra = extra, fo = fo, perm = perm};
 
 (*
 Remarks:
   - elhs is used for matching,
     lhs only for preservation of bound variable names;
   - fo is set iff
     either elhs is first-order (no Var is applied),
       in which case fo-matching is complete,
     or elhs is not a pattern,
       in which case there is nothing better to do;
 *)
 
 fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
   Thm.eq_thm_prop (thm1, thm2);
 
 (* FIXME: it seems that the conditions on extra variables are too liberal if
 prems are nonempty: does solving the prems really guarantee instantiation of
 all its Vars? Better: a dynamic check each time a rule is applied.
 *)
 fun rewrite_rule_extra_vars prems elhs erhs =
   let
     val elhss = elhs :: prems;
     val tvars = TVars.build (fold TVars.add_tvars elhss);
     val vars = Vars.build (fold Vars.add_vars elhss);
   in
     erhs |> Term.exists_type (Term.exists_subtype
       (fn TVar v => not (TVars.defined tvars v) | _ => false)) orelse
     erhs |> Term.exists_subterm
       (fn Var v => not (Vars.defined vars v) | _ => false)
   end;
 
 fun rrule_extra_vars elhs thm =
   rewrite_rule_extra_vars [] (Thm.term_of elhs) (Thm.full_prop_of thm);
 
 fun mk_rrule2 {thm, name, lhs, elhs, perm} =
   let
     val t = Thm.term_of elhs;
     val fo = Pattern.first_order t orelse not (Pattern.pattern t);
     val extra = rrule_extra_vars elhs thm;
   in {thm = thm, name = name, lhs = lhs, elhs = elhs, extra = extra, fo = fo, perm = perm} end;
 
 (*simple test for looping rewrite rules and stupid orientations*)
 fun default_reorient ctxt prems lhs rhs =
   rewrite_rule_extra_vars prems lhs rhs
     orelse
   is_Var (head_of lhs)
     orelse
 (* turns t = x around, which causes a headache if x is a local variable -
    usually it is very useful :-(
   is_Free rhs andalso not(is_Free lhs) andalso not(Logic.occs(rhs,lhs))
   andalso not(exists_subterm is_Var lhs)
     orelse
 *)
   exists (fn t => Logic.occs (lhs, t)) (rhs :: prems)
     orelse
   null prems andalso Pattern.matches (Proof_Context.theory_of ctxt) (lhs, rhs)
     (*the condition "null prems" is necessary because conditional rewrites
       with extra variables in the conditions may terminate although
       the rhs is an instance of the lhs; example: ?m < ?n \<Longrightarrow> f ?n \<equiv> f ?m *)
     orelse
   is_Const lhs andalso not (is_Const rhs);
 
 
 (* simplification procedures *)
 
 datatype proc =
   Proc of
    {name: string,
     lhs: term,
     proc: Proof.context -> cterm -> thm option,
     stamp: stamp};
 
 fun eq_proc (Proc {stamp = stamp1, ...}, Proc {stamp = stamp2, ...}) = stamp1 = stamp2;
 
 
 (* solvers *)
 
 datatype solver =
   Solver of
    {name: string,
     solver: Proof.context -> int -> tactic,
     id: stamp};
 
 fun mk_solver name solver = Solver {name = name, solver = solver, id = stamp ()};
 
 fun solver_name (Solver {name, ...}) = name;
 fun solver ctxt (Solver {solver = tac, ...}) = tac ctxt;
 fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2);
 
 
 (* simplification sets *)
 
 (*A simpset contains data required during conversion:
     rules: discrimination net of rewrite rules;
     prems: current premises;
     depth: simp_depth and exceeded flag;
     congs: association list of congruence rules and
            a list of `weak' congruence constants.
            A congruence is `weak' if it avoids normalization of some argument.
     procs: discrimination net of simplification procedures
       (functions that prove rewrite rules on the fly);
     mk_rews:
       mk: turn simplification thms into rewrite rules;
       mk_cong: prepare congruence rules;
       mk_sym: turn \<equiv> around;
       mk_eq_True: turn P into P \<equiv> True;
     term_ord: for ordered rewriting;*)
 
 datatype simpset =
   Simpset of
    {rules: rrule Net.net,
     prems: thm list,
     depth: int * bool Unsynchronized.ref} *
    {congs: thm Congtab.table * cong_name list,
     procs: proc Net.net,
     mk_rews:
      {mk: Proof.context -> thm -> thm list,
       mk_cong: Proof.context -> thm -> thm,
       mk_sym: Proof.context -> thm -> thm option,
       mk_eq_True: Proof.context -> thm -> thm option,
       reorient: Proof.context -> term list -> term -> term -> bool},
     term_ord: term ord,
     subgoal_tac: Proof.context -> int -> tactic,
     loop_tacs: (string * (Proof.context -> int -> tactic)) list,
     solvers: solver list * solver list};
 
 fun internal_ss (Simpset (_, ss2)) = ss2;
 
 fun make_ss1 (rules, prems, depth) = {rules = rules, prems = prems, depth = depth};
 
 fun map_ss1 f {rules, prems, depth} = make_ss1 (f (rules, prems, depth));
 
 fun make_ss2 (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =
   {congs = congs, procs = procs, mk_rews = mk_rews, term_ord = term_ord,
     subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers};
 
 fun map_ss2 f {congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers} =
   make_ss2 (f (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers));
 
 fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2);
 
 fun dest_ss (Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...})) =
  {simps = Net.entries rules
     |> map (fn {name, thm, ...} => (name, thm)),
   procs = Net.entries procs
     |> map (fn Proc {name, lhs, stamp, ...} => ((name, lhs), stamp))
     |> partition_eq (eq_snd op =)
     |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)),
   congs = congs |> fst |> Congtab.dest,
   weak_congs = congs |> snd,
   loopers = map fst loop_tacs,
   unsafe_solvers = map solver_name (#1 solvers),
   safe_solvers = map solver_name (#2 solvers)};
 
 
 (* empty *)
 
 fun init_ss depth mk_rews term_ord subgoal_tac solvers =
   make_simpset ((Net.empty, [], depth),
     ((Congtab.empty, []), Net.empty, mk_rews, term_ord, subgoal_tac, [], solvers));
 
 fun default_mk_sym _ th = SOME (th RS Drule.symmetric_thm);
 
 val empty_ss =
   init_ss (0, Unsynchronized.ref false)
     {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
       mk_cong = K I,
       mk_sym = default_mk_sym,
       mk_eq_True = K (K NONE),
       reorient = default_reorient}
     Term_Ord.term_ord (K (K no_tac)) ([], []);
 
 
 (* merge *)  (*NOTE: ignores some fields of 2nd simpset*)
 
 fun merge_ss (ss1, ss2) =
   if pointer_eq (ss1, ss2) then ss1
   else
     let
       val Simpset ({rules = rules1, prems = prems1, depth = depth1},
        {congs = (congs1, weak1), procs = procs1, mk_rews, term_ord, subgoal_tac,
         loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
       val Simpset ({rules = rules2, prems = prems2, depth = depth2},
        {congs = (congs2, weak2), procs = procs2, mk_rews = _, term_ord = _, subgoal_tac = _,
         loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
 
       val rules' = Net.merge eq_rrule (rules1, rules2);
       val prems' = Thm.merge_thms (prems1, prems2);
       val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
       val congs' = Congtab.merge (K true) (congs1, congs2);
       val weak' = merge (op =) (weak1, weak2);
       val procs' = Net.merge eq_proc (procs1, procs2);
       val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
       val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2);
       val solvers' = merge eq_solver (solvers1, solvers2);
     in
       make_simpset ((rules', prems', depth'), ((congs', weak'), procs',
         mk_rews, term_ord, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
     end;
 
 
 
 (** context data **)
 
 structure Simpset = Generic_Data
 (
   type T = simpset;
   val empty = empty_ss;
   val merge = merge_ss;
 );
 
 val simpset_of = Simpset.get o Context.Proof;
 
 fun map_simpset f = Context.proof_map (Simpset.map f);
 fun map_simpset1 f = map_simpset (fn Simpset (ss1, ss2) => Simpset (map_ss1 f ss1, ss2));
 fun map_simpset2 f = map_simpset (fn Simpset (ss1, ss2) => Simpset (ss1, map_ss2 f ss2));
 
 fun put_simpset ss = map_simpset (K ss);
 
 fun simpset_map ctxt f ss = ctxt |> put_simpset ss |> f |> simpset_of;
 
 val empty_simpset = put_simpset empty_ss;
 
 fun map_theory_simpset f thy =
   let
     val ctxt' = f (Proof_Context.init_global thy);
     val thy' = Proof_Context.theory_of ctxt';
   in Context.theory_map (Simpset.map (K (simpset_of ctxt'))) thy' end;
 
 fun map_ss f = Context.mapping (map_theory_simpset (f o Context_Position.not_really)) f;
 
 val clear_simpset =
   map_simpset (fn Simpset ({depth, ...}, {mk_rews, term_ord, subgoal_tac, solvers, ...}) =>
     init_ss depth mk_rews term_ord subgoal_tac solvers);
 
 
 (* accessors for tactis *)
 
 fun subgoal_tac ctxt = (#subgoal_tac o internal_ss o simpset_of) ctxt ctxt;
 
 fun loop_tac ctxt =
   FIRST' (map (fn (_, tac) => tac ctxt) (rev ((#loop_tacs o internal_ss o simpset_of) ctxt)));
 
 val solvers = #solvers o internal_ss o simpset_of
 
 
 (* simp depth *)
 
 (*
 The simp_depth_limit is meant to abort infinite recursion of the simplifier
 early but should not terminate "normal" executions.
 As of 2017, 25 would suffice; 40 builds in a safety margin.
 *)
 
 val simp_depth_limit = Config.declare_int ("simp_depth_limit", \<^here>) (K 40);
 val simp_trace_depth_limit = Config.declare_int ("simp_trace_depth_limit", \<^here>) (K 1);
 
 fun inc_simp_depth ctxt =
   ctxt |> map_simpset1 (fn (rules, prems, (depth, exceeded)) =>
     (rules, prems,
       (depth + 1,
         if depth = Config.get ctxt simp_trace_depth_limit
         then Unsynchronized.ref false else exceeded)));
 
 fun simp_depth ctxt =
   let val Simpset ({depth = (depth, _), ...}, _) = simpset_of ctxt
   in depth end;
 
 
 (* diagnostics *)
 
 exception SIMPLIFIER of string * thm list;
 
 val simp_debug = Config.declare_bool ("simp_debug", \<^here>) (K false);
 val simp_trace = Config.declare_bool ("simp_trace", \<^here>) (K false);
 
 fun cond_warning ctxt msg =
   if Context_Position.is_really_visible ctxt then warning (msg ()) else ();
 
 fun cond_tracing' ctxt flag msg =
   if Config.get ctxt flag then
     let
       val Simpset ({depth = (depth, exceeded), ...}, _) = simpset_of ctxt;
       val depth_limit = Config.get ctxt simp_trace_depth_limit;
     in
       if depth > depth_limit then
         if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true)
       else (tracing (enclose "[" "]" (string_of_int depth) ^ msg ()); exceeded := false)
     end
   else ();
 
 fun cond_tracing ctxt = cond_tracing' ctxt simp_trace;
 
 fun print_term ctxt s t =
   s ^ "\n" ^ Syntax.string_of_term ctxt t;
 
 fun print_thm ctxt s (name, th) =
   print_term ctxt (if name = "" then s else s ^ " " ^ quote name ^ ":") (Thm.full_prop_of th);
 
 
 
 (** simpset operations **)
 
 (* prems *)
 
 fun prems_of ctxt =
   let val Simpset ({prems, ...}, _) = simpset_of ctxt in prems end;
 
 fun add_prems ths =
   map_simpset1 (fn (rules, prems, depth) => (rules, ths @ prems, depth));
 
 
 (* maintain simp rules *)
 
 fun del_rrule loud (rrule as {thm, elhs, ...}) ctxt =
   ctxt |> map_simpset1 (fn (rules, prems, depth) =>
     (Net.delete_term eq_rrule (Thm.term_of elhs, rrule) rules, prems, depth))
   handle Net.DELETE =>
     (if not loud then ()
      else cond_warning ctxt
             (fn () => print_thm ctxt "Rewrite rule not in simpset:" ("", thm));
      ctxt);
 
 fun insert_rrule (rrule as {thm, name, ...}) ctxt =
  (cond_tracing ctxt (fn () => print_thm ctxt "Adding rewrite rule" (name, thm));
   ctxt |> map_simpset1 (fn (rules, prems, depth) =>
     let
       val rrule2 as {elhs, ...} = mk_rrule2 rrule;
       val rules' = Net.insert_term eq_rrule (Thm.term_of elhs, trim_context_rrule rrule2) rules;
     in (rules', prems, depth) end)
   handle Net.INSERT =>
     (cond_warning ctxt (fn () => print_thm ctxt "Ignoring duplicate rewrite rule:" ("", thm));
       ctxt));
 
 val vars_set = Vars.build o Vars.add_vars;
 
 local
 
 fun vperm (Var _, Var _) = true
   | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
   | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
   | vperm (t, u) = (t = u);
 
 fun var_perm (t, u) = vperm (t, u) andalso Vars.eq_set (apply2 vars_set (t, u));
 
 in
 
 fun decomp_simp thm =
   let
     val prop = Thm.prop_of thm;
     val prems = Logic.strip_imp_prems prop;
     val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
     val (lhs, rhs) = Thm.dest_equals concl handle TERM _ =>
       raise SIMPLIFIER ("Rewrite rule not a meta-equality", [thm]);
     val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs));
     val erhs = Envir.eta_contract (Thm.term_of rhs);
     val perm =
       var_perm (Thm.term_of elhs, erhs) andalso
       not (Thm.term_of elhs aconv erhs) andalso
       not (is_Var (Thm.term_of elhs));
   in (prems, Thm.term_of lhs, elhs, Thm.term_of rhs, perm) end;
 
 end;
 
 fun decomp_simp' thm =
   let val (_, lhs, _, rhs, _) = decomp_simp thm in
     if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", [thm])
     else (lhs, rhs)
   end;
 
 fun mk_eq_True ctxt (thm, name) =
   let val Simpset (_, {mk_rews = {mk_eq_True, ...}, ...}) = simpset_of ctxt in
     (case mk_eq_True ctxt thm of
       NONE => []
     | SOME eq_True =>
         let val (_, lhs, elhs, _, _) = decomp_simp eq_True;
         in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end)
   end;
 
 (*create the rewrite rule and possibly also the eq_True variant,
   in case there are extra vars on the rhs*)
 fun rrule_eq_True ctxt thm name lhs elhs rhs thm2 =
   let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in
     if rewrite_rule_extra_vars [] lhs rhs then
       mk_eq_True ctxt (thm2, name) @ [rrule]
     else [rrule]
   end;
 
 fun mk_rrule ctxt (thm, name) =
   let val (prems, lhs, elhs, rhs, perm) = decomp_simp thm in
     if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
     else
       (*weak test for loops*)
       if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (Thm.term_of elhs)
       then mk_eq_True ctxt (thm, name)
       else rrule_eq_True ctxt thm name lhs elhs rhs thm
   end |> map (fn {thm, name, lhs, elhs, perm} =>
     {thm = Thm.trim_context thm, name = name, lhs = lhs,
       elhs = Thm.trim_context_cterm elhs, perm = perm});
 
 fun orient_rrule ctxt (thm, name) =
   let
     val (prems, lhs, elhs, rhs, perm) = decomp_simp thm;
     val Simpset (_, {mk_rews = {reorient, mk_sym, ...}, ...}) = simpset_of ctxt;
   in
     if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
     else if reorient ctxt prems lhs rhs then
       if reorient ctxt prems rhs lhs
       then mk_eq_True ctxt (thm, name)
       else
         (case mk_sym ctxt thm of
           NONE => []
         | SOME thm' =>
             let val (_, lhs', elhs', rhs', _) = decomp_simp thm'
             in rrule_eq_True ctxt thm' name lhs' elhs' rhs' thm end)
     else rrule_eq_True ctxt thm name lhs elhs rhs thm
   end;
 
 fun extract_rews ctxt sym thms =
   let
     val Simpset (_, {mk_rews = {mk, ...}, ...}) = simpset_of ctxt;
     val mk =
       if sym then fn ctxt => fn th => (mk ctxt th) RL [Drule.symmetric_thm]
       else mk
   in maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ctxt thm)) thms
   end;
 
 fun extract_safe_rrules ctxt thm =
   maps (orient_rrule ctxt) (extract_rews ctxt false [thm]);
 
 fun mk_rrules ctxt thms =
   let
     val rews = extract_rews ctxt false thms
     val raw_rrules = flat (map (mk_rrule ctxt) rews)
   in map mk_rrule2 raw_rrules end
 
 
 (* add/del rules explicitly *)
 
 local
 
 fun comb_simps ctxt comb mk_rrule sym thms =
   let val rews = extract_rews ctxt sym (map (Thm.transfer' ctxt) thms);
   in fold (fold comb o mk_rrule) rews ctxt end;
 
 (*
 This code checks if the symetric version of a rule is already in the simpset.
 However, the variable names in the two versions of the rule may differ.
 Thus the current test modulo eq_rrule is too weak to be useful
 and needs to be refined.
 
 fun present ctxt rules (rrule as {thm, elhs, ...}) =
   (Net.insert_term eq_rrule (Thm.term_of elhs, trim_context_rrule rrule) rules;
    false)
   handle Net.INSERT =>
     (cond_warning ctxt
        (fn () => print_thm ctxt "Symmetric rewrite rule already in simpset:" ("", thm));
      true);
 
 fun sym_present ctxt thms =
   let
     val rews = extract_rews ctxt true (map (Thm.transfer' ctxt) thms);
     val rrules = map mk_rrule2 (flat(map (mk_rrule ctxt) rews))
     val Simpset({rules, ...},_) = simpset_of ctxt
   in exists (present ctxt rules) rrules end
 *)
 in
 
 fun ctxt addsimps thms =
   comb_simps ctxt insert_rrule (mk_rrule ctxt) false thms;
 
 fun addsymsimps ctxt thms =
   comb_simps ctxt insert_rrule (mk_rrule ctxt) true thms;
 
 fun ctxt delsimps thms =
   comb_simps ctxt (del_rrule true) (map mk_rrule2 o mk_rrule ctxt) false thms;
 
 fun delsimps_quiet ctxt thms =
   comb_simps ctxt (del_rrule false) (map mk_rrule2 o mk_rrule ctxt) false thms;
 
 fun add_simp thm ctxt = ctxt addsimps [thm];
 (*
 with check for presence of symmetric version:
   if sym_present ctxt [thm]
   then (cond_warning ctxt (fn () => print_thm ctxt "Ignoring rewrite rule:" ("", thm)); ctxt)
   else ctxt addsimps [thm];
 *)
 fun del_simp thm ctxt = ctxt delsimps [thm];
 fun flip_simp thm ctxt = addsymsimps (delsimps_quiet ctxt [thm]) [thm];
 
 end;
 
 fun init_simpset thms ctxt = ctxt
   |> Context_Position.set_visible false
   |> empty_simpset
   |> fold add_simp thms
   |> Context_Position.restore_visible ctxt;
 
 
 (* congs *)
 
 local
 
 fun is_full_cong_prems [] [] = true
   | is_full_cong_prems [] _ = false
   | is_full_cong_prems (p :: prems) varpairs =
       (case Logic.strip_assums_concl p of
         Const ("Pure.eq", _) $ lhs $ rhs =>
           let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in
             is_Var x andalso forall is_Bound xs andalso
             not (has_duplicates (op =) xs) andalso xs = ys andalso
             member (op =) varpairs (x, y) andalso
             is_full_cong_prems prems (remove (op =) (x, y) varpairs)
           end
       | _ => false);
 
 fun is_full_cong thm =
   let
     val prems = Thm.prems_of thm and concl = Thm.concl_of thm;
     val (lhs, rhs) = Logic.dest_equals concl;
     val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs;
   in
     f = g andalso not (has_duplicates (op =) (xs @ ys)) andalso length xs = length ys andalso
     is_full_cong_prems prems (xs ~~ ys)
   end;
 
 fun mk_cong ctxt =
   let val Simpset (_, {mk_rews = {mk_cong = f, ...}, ...}) = simpset_of ctxt
   in f ctxt end;
 
 in
 
 fun add_eqcong thm ctxt = ctxt |> map_simpset2
   (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
     let
       val (lhs, _) = Logic.dest_equals (Thm.concl_of thm)
         handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", [thm]);
     (*val lhs = Envir.eta_contract lhs;*)
       val a = the (cong_name (head_of lhs)) handle Option.Option =>
         raise SIMPLIFIER ("Congruence must start with a constant or free variable", [thm]);
       val (xs, weak) = congs;
       val xs' = Congtab.update (a, Thm.trim_context thm) xs;
       val weak' = if is_full_cong thm then weak else a :: weak;
     in ((xs', weak'), procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) end);
 
 fun del_eqcong thm ctxt = ctxt |> map_simpset2
   (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
     let
       val (lhs, _) = Logic.dest_equals (Thm.concl_of thm)
         handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", [thm]);
     (*val lhs = Envir.eta_contract lhs;*)
       val a = the (cong_name (head_of lhs)) handle Option.Option =>
         raise SIMPLIFIER ("Congruence must start with a constant", [thm]);
       val (xs, _) = congs;
       val xs' = Congtab.delete_safe a xs;
       val weak' = Congtab.fold (fn (a, th) => if is_full_cong th then I else insert (op =) a) xs' [];
     in ((xs', weak'), procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) end);
 
 fun add_cong thm ctxt = add_eqcong (mk_cong ctxt thm) ctxt;
 fun del_cong thm ctxt = del_eqcong (mk_cong ctxt thm) ctxt;
 
 end;
 
 
 (* simprocs *)
 
 datatype simproc =
   Simproc of
     {name: string,
      lhss: term list,
      proc: (Proof.context -> cterm -> thm option) Morphism.entity,
      stamp: stamp};
 
 fun eq_simproc (Simproc {stamp = stamp1, ...}, Simproc {stamp = stamp2, ...}) = stamp1 = stamp2;
 
 fun cert_simproc thy name {lhss, proc} =
   Simproc {name = name, lhss = map (Sign.cert_term thy) lhss, proc = proc, stamp = stamp ()};
 
 fun transform_simproc phi (Simproc {name, lhss, proc, stamp}) =
   Simproc
    {name = name,
     lhss = map (Morphism.term phi) lhss,
     proc = Morphism.transform_reset_context phi proc,
     stamp = stamp};
 
 local
 
 fun add_proc (proc as Proc {name, lhs, ...}) ctxt =
  (cond_tracing ctxt (fn () =>
     print_term ctxt ("Adding simplification procedure " ^ quote name ^ " for") lhs);
   ctxt |> map_simpset2
     (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
       (congs, Net.insert_term eq_proc (lhs, proc) procs,
         mk_rews, term_ord, subgoal_tac, loop_tacs, solvers))
   handle Net.INSERT =>
     (cond_warning ctxt (fn () => "Ignoring duplicate simplification procedure " ^ quote name);
       ctxt));
 
 fun del_proc (proc as Proc {name, lhs, ...}) ctxt =
   ctxt |> map_simpset2
     (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
       (congs, Net.delete_term eq_proc (lhs, proc) procs,
         mk_rews, term_ord, subgoal_tac, loop_tacs, solvers))
   handle Net.DELETE =>
     (cond_warning ctxt (fn () => "Simplification procedure " ^ quote name ^ " not in simpset");
       ctxt);
 
 fun prep_procs (Simproc {name, lhss, proc, stamp}) =
   lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, stamp = stamp});
 
 in
 
 fun ctxt addsimprocs ps = fold (fold add_proc o prep_procs) ps ctxt;
 fun ctxt delsimprocs ps = fold (fold del_proc o prep_procs) ps ctxt;
 
 end;
 
 
 (* mk_rews *)
 
 local
 
 fun map_mk_rews f =
   map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
     let
       val {mk, mk_cong, mk_sym, mk_eq_True, reorient} = mk_rews;
       val (mk', mk_cong', mk_sym', mk_eq_True', reorient') =
         f (mk, mk_cong, mk_sym, mk_eq_True, reorient);
       val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True',
         reorient = reorient'};
     in (congs, procs, mk_rews', term_ord, subgoal_tac, loop_tacs, solvers) end);
 
 in
 
 fun mksimps ctxt =
   let val Simpset (_, {mk_rews = {mk, ...}, ...}) = simpset_of ctxt
   in mk ctxt end;
 
 fun set_mksimps mk = map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
 
 fun set_mkcong mk_cong = map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) =>
   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
 
 fun set_mksym mk_sym = map_mk_rews (fn (mk, mk_cong, _, mk_eq_True, reorient) =>
   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
 
 fun set_mkeqTrue mk_eq_True = map_mk_rews (fn (mk, mk_cong, mk_sym, _, reorient) =>
   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
 
 fun set_reorient reorient = map_mk_rews (fn (mk, mk_cong, mk_sym, mk_eq_True, _) =>
   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
 
 end;
 
 
 (* term_ord *)
 
 fun set_term_ord term_ord =
   map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) =>
    (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers));
 
 
 (* tactics *)
 
 fun set_subgoaler subgoal_tac =
   map_simpset2 (fn (congs, procs, mk_rews, term_ord, _, loop_tacs, solvers) =>
    (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers));
 
 fun ctxt setloop tac = ctxt |>
   map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, _, solvers) =>
    (congs, procs, mk_rews, term_ord, subgoal_tac, [("", tac)], solvers));
 
 fun ctxt addloop (name, tac) = ctxt |>
   map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
     (congs, procs, mk_rews, term_ord, subgoal_tac,
      AList.update (op =) (name, tac) loop_tacs, solvers));
 
 fun ctxt delloop name = ctxt |>
   map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
     (congs, procs, mk_rews, term_ord, subgoal_tac,
      (if AList.defined (op =) loop_tacs name then ()
       else cond_warning ctxt (fn () => "No such looper in simpset: " ^ quote name);
       AList.delete (op =) name loop_tacs), solvers));
 
 fun ctxt setSSolver solver = ctxt |> map_simpset2
   (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
     (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));
 
 fun ctxt addSSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, term_ord,
   subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, term_ord,
     subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers)));
 
 fun ctxt setSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, term_ord,
   subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, term_ord,
     subgoal_tac, loop_tacs, ([solver], solvers)));
 
 fun ctxt addSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, term_ord,
   subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, term_ord,
     subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers)));
 
 fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, term_ord,
   subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, term_ord,
   subgoal_tac, loop_tacs, (solvers, solvers)));
 
 
 (* trace operations *)
 
 type trace_ops =
  {trace_invoke: {depth: int, term: term} -> Proof.context -> Proof.context,
   trace_apply: {unconditional: bool, term: term, thm: thm, rrule: rrule} ->
     Proof.context -> (Proof.context -> (thm * term) option) -> (thm * term) option};
 
 structure Trace_Ops = Theory_Data
 (
   type T = trace_ops;
   val empty: T =
    {trace_invoke = fn _ => fn ctxt => ctxt,
     trace_apply = fn _ => fn ctxt => fn cont => cont ctxt};
   fun merge (trace_ops, _) = trace_ops;
 );
 
 val set_trace_ops = Trace_Ops.put;
 
 val trace_ops = Trace_Ops.get o Proof_Context.theory_of;
 fun trace_invoke args ctxt = #trace_invoke (trace_ops ctxt) args ctxt;
 fun trace_apply args ctxt = #trace_apply (trace_ops ctxt) args ctxt;
 
 
 
 (** rewriting **)
 
 (*
   Uses conversions, see:
     L C Paulson, A higher-order implementation of rewriting,
     Science of Computer Programming 3 (1983), pages 119-149.
 *)
 
 fun check_conv ctxt msg thm thm' =
   let
     val thm'' = Thm.transitive thm thm' handle THM _ =>
       let
         val nthm' =
           Thm.transitive (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm'
       in Thm.transitive thm nthm' handle THM _ =>
            let
              val nthm =
                Thm.transitive thm (Drule.beta_eta_conversion (Thm.rhs_of thm))
            in Thm.transitive nthm nthm' end
       end
     val _ =
       if msg then cond_tracing ctxt (fn () => print_thm ctxt "SUCCEEDED" ("", thm'))
       else ();
   in SOME thm'' end
   handle THM _ =>
     let
       val _ $ _ $ prop0 = Thm.prop_of thm;
       val _ =
         cond_tracing ctxt (fn () =>
           print_thm ctxt "Proved wrong theorem (bad subgoaler?)" ("", thm') ^ "\n" ^
           print_term ctxt "Should have proved:" prop0);
     in NONE end;
 
 
 (* mk_procrule *)
 
 fun mk_procrule ctxt thm =
   let
     val (prems, lhs, elhs, rhs, _) = decomp_simp thm
     val thm' = Thm.close_derivation \<^here> thm;
   in
     if rewrite_rule_extra_vars prems lhs rhs
     then (cond_warning ctxt (fn () => print_thm ctxt "Extra vars on rhs:" ("", thm)); [])
     else [mk_rrule2 {thm = thm', name = "", lhs = lhs, elhs = elhs, perm = false}]
   end;
 
 
 (* rewritec: conversion to apply the meta simpset to a term *)
 
 (*Since the rewriting strategy is bottom-up, we avoid re-normalizing already
   normalized terms by carrying around the rhs of the rewrite rule just
   applied. This is called the `skeleton'. It is decomposed in parallel
   with the term. Once a Var is encountered, the corresponding term is
   already in normal form.
   skel0 is a dummy skeleton that is to enforce complete normalization.*)
 
 val skel0 = Bound 0;
 
 (*Use rhs as skeleton only if the lhs does not contain unnormalized bits.
   The latter may happen iff there are weak congruence rules for constants
   in the lhs.*)
 
 fun uncond_skel ((_, weak), (lhs, rhs)) =
   if null weak then rhs  (*optimization*)
   else if exists_subterm
     (fn Const (a, _) => member (op =) weak (true, a)
       | Free (a, _) => member (op =) weak (false, a)
       | _ => false) lhs then skel0
   else rhs;
 
 (*Behaves like unconditional rule if rhs does not contain vars not in the lhs.
   Otherwise those vars may become instantiated with unnormalized terms
   while the premises are solved.*)
 
 fun cond_skel (args as (_, (lhs, rhs))) =
   if Vars.subset (vars_set rhs, vars_set lhs) then uncond_skel args
   else skel0;
 
 (*
   Rewriting -- we try in order:
     (1) beta reduction
     (2) unconditional rewrite rules
     (3) conditional rewrite rules
     (4) simplification procedures
 
   IMPORTANT: rewrite rules must not introduce new Vars or TVars!
 *)
 
 fun rewritec (prover, maxt) ctxt t =
   let
     val thy = Proof_Context.theory_of ctxt;
     val Simpset ({rules, ...}, {congs, procs, term_ord, ...}) = simpset_of ctxt;
     val eta_thm = Thm.eta_conversion t;
     val eta_t' = Thm.rhs_of eta_thm;
     val eta_t = Thm.term_of eta_t';
     fun rew rrule =
       let
         val {thm = thm0, name, lhs, elhs = elhs0, extra, fo, perm} = rrule;
         val thm = Thm.transfer thy thm0;
         val elhs = Thm.transfer_cterm thy elhs0;
         val prop = Thm.prop_of thm;
         val (rthm, elhs') =
           if maxt = ~1 orelse not extra then (thm, elhs)
           else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs);
 
         val insts =
           if fo then Thm.first_order_match (elhs', eta_t')
           else Thm.match (elhs', eta_t');
         val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
         val prop' = Thm.prop_of thm';
         val unconditional = Logic.no_prems prop';
         val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop');
         val trace_args = {unconditional = unconditional, term = eta_t, thm = thm', rrule = rrule};
       in
         if perm andalso is_greater_equal (term_ord (rhs', lhs'))
         then
          (cond_tracing ctxt (fn () =>
             print_thm ctxt "Cannot apply permutative rewrite rule" (name, thm) ^ "\n" ^
             print_thm ctxt "Term does not become smaller:" ("", thm'));
           NONE)
         else
          (cond_tracing ctxt (fn () =>
             print_thm ctxt "Applying instance of rewrite rule" (name, thm));
           if unconditional
           then
            (cond_tracing ctxt (fn () => print_thm ctxt "Rewriting:" ("", thm'));
             trace_apply trace_args ctxt (fn ctxt' =>
               let
                 val lr = Logic.dest_equals prop;
                 val SOME thm'' = check_conv ctxt' false eta_thm thm';
               in SOME (thm'', uncond_skel (congs, lr)) end))
           else
            (cond_tracing ctxt (fn () => print_thm ctxt "Trying to rewrite:" ("", thm'));
             if simp_depth ctxt > Config.get ctxt simp_depth_limit
             then (cond_tracing ctxt (fn () => "simp_depth_limit exceeded - giving up"); NONE)
             else
               trace_apply trace_args ctxt (fn ctxt' =>
                 (case prover ctxt' thm' of
                   NONE => (cond_tracing ctxt' (fn () => print_thm ctxt' "FAILED" ("", thm')); NONE)
                 | SOME thm2 =>
                     (case check_conv ctxt' true eta_thm thm2 of
                       NONE => NONE
                     | SOME thm2' =>
                         let
                           val concl = Logic.strip_imp_concl prop;
                           val lr = Logic.dest_equals concl;
                         in SOME (thm2', cond_skel (congs, lr)) end)))))
       end;
 
     fun rews [] = NONE
       | rews (rrule :: rrules) =
           let val opt = rew rrule handle Pattern.MATCH => NONE
           in (case opt of NONE => rews rrules | some => some) end;
 
     fun sort_rrules rrs =
       let
         fun is_simple ({thm, ...}: rrule) =
           (case Thm.prop_of thm of
             Const ("Pure.eq", _) $ _ $ _ => true
           | _ => false);
         fun sort [] (re1, re2) = re1 @ re2
           | sort (rr :: rrs) (re1, re2) =
               if is_simple rr
               then sort rrs (rr :: re1, re2)
               else sort rrs (re1, rr :: re2);
       in sort rrs ([], []) end;
 
     fun proc_rews [] = NONE
       | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
           if Pattern.matches (Proof_Context.theory_of ctxt) (lhs, Thm.term_of t) then
             (cond_tracing' ctxt simp_debug (fn () =>
               print_term ctxt ("Trying procedure " ^ quote name ^ " on:") eta_t);
              (case proc ctxt eta_t' of
                NONE => (cond_tracing' ctxt simp_debug (fn () => "FAILED"); proc_rews ps)
              | SOME raw_thm =>
                  (cond_tracing ctxt (fn () =>
                     print_thm ctxt ("Procedure " ^ quote name ^ " produced rewrite rule:")
                       ("", raw_thm));
                   (case rews (mk_procrule ctxt raw_thm) of
                     NONE =>
                      (cond_tracing ctxt (fn () =>
                         print_term ctxt ("IGNORED result of simproc " ^ quote name ^
                             " -- does not match") (Thm.term_of t));
                       proc_rews ps)
                   | some => some))))
           else proc_rews ps;
   in
     (case eta_t of
       Abs _ $ _ => SOME (Thm.transitive eta_thm (Thm.beta_conversion false eta_t'), skel0)
     | _ =>
       (case rews (sort_rrules (Net.match_term rules eta_t)) of
         NONE => proc_rews (Net.match_term procs eta_t)
       | some => some))
   end;
 
 
 (* conversion to apply a congruence rule to a term *)
 
 fun congc prover ctxt maxt cong t =
   let
     val rthm = Thm.incr_indexes (maxt + 1) cong;
     val rlhs = fst (Thm.dest_equals (Drule.strip_imp_concl (Thm.cprop_of rthm)));
     val insts = Thm.match (rlhs, t)
     (* Thm.match can raise Pattern.MATCH;
        is handled when congc is called *)
     val thm' =
       Thm.instantiate insts (Thm.rename_boundvars (Thm.term_of rlhs) (Thm.term_of t) rthm);
     val _ =
       cond_tracing ctxt (fn () => print_thm ctxt "Applying congruence rule:" ("", thm'));
     fun err (msg, thm) = (cond_tracing ctxt (fn () => print_thm ctxt msg ("", thm)); NONE);
   in
     (case prover thm' of
       NONE => err ("Congruence proof failed.  Could not prove", thm')
     | SOME thm2 =>
         (case check_conv ctxt true (Drule.beta_eta_conversion t) thm2 of
           NONE => err ("Congruence proof failed.  Should not have proved", thm2)
         | SOME thm2' =>
             if op aconv (apply2 Thm.term_of (Thm.dest_equals (Thm.cprop_of thm2')))
             then NONE else SOME thm2'))
   end;
 
 val vA = (("A", 0), propT);
 val vB = (("B", 0), propT);
 val vC = (("C", 0), propT);
 
 fun transitive1 NONE NONE = NONE
   | transitive1 (SOME thm1) NONE = SOME thm1
   | transitive1 NONE (SOME thm2) = SOME thm2
   | transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2);
 
 fun transitive2 thm = transitive1 (SOME thm);
 fun transitive3 thm = transitive1 thm o SOME;
 
 fun bottomc ((simprem, useprem, mutsimp), prover, maxidx) =
   let
     fun botc skel ctxt t =
       if is_Var skel then NONE
       else
         (case subc skel ctxt t of
            some as SOME thm1 =>
              (case rewritec (prover, maxidx) ctxt (Thm.rhs_of thm1) of
                 SOME (thm2, skel2) =>
                   transitive2 (Thm.transitive thm1 thm2)
                     (botc skel2 ctxt (Thm.rhs_of thm2))
               | NONE => some)
          | NONE =>
              (case rewritec (prover, maxidx) ctxt t of
                 SOME (thm2, skel2) => transitive2 thm2
                   (botc skel2 ctxt (Thm.rhs_of thm2))
               | NONE => NONE))
 
     and try_botc ctxt t =
       (case botc skel0 ctxt t of
         SOME trec1 => trec1
       | NONE => Thm.reflexive t)
 
     and subc skel ctxt t0 =
         let val Simpset (_, {congs, ...}) = simpset_of ctxt in
           (case Thm.term_of t0 of
               Abs (a, _, _) =>
                 let
                   val ((v, t'), ctxt') = Variable.dest_abs_cterm t0 ctxt;
                   val skel' = (case skel of Abs (_, _, sk) => sk | _ => skel0);
                 in
                   (case botc skel' ctxt' t' of
                     SOME thm => SOME (Thm.abstract_rule a v thm)
                   | NONE => NONE)
                 end
             | t $ _ =>
               (case t of
                 Const ("Pure.imp", _) $ _  => impc t0 ctxt
               | Abs _ =>
                   let val thm = Thm.beta_conversion false t0
                   in
                     (case subc skel0 ctxt (Thm.rhs_of thm) of
                       NONE => SOME thm
                     | SOME thm' => SOME (Thm.transitive thm thm'))
                   end
               | _  =>
                   let
                     fun appc () =
                       let
                         val (tskel, uskel) =
                           (case skel of
                             tskel $ uskel => (tskel, uskel)
                           | _ => (skel0, skel0));
                         val (ct, cu) = Thm.dest_comb t0;
                       in
                         (case botc tskel ctxt ct of
                           SOME thm1 =>
                             (case botc uskel ctxt cu of
                               SOME thm2 => SOME (Thm.combination thm1 thm2)
                             | NONE => SOME (Thm.combination thm1 (Thm.reflexive cu)))
                         | NONE =>
                             (case botc uskel ctxt cu of
                               SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1)
                             | NONE => NONE))
                       end;
                     val (h, ts) = strip_comb t;
                   in
                     (case cong_name h of
                       SOME a =>
                         (case Congtab.lookup (fst congs) a of
                           NONE => appc ()
                         | SOME cong =>
      (*post processing: some partial applications h t1 ... tj, j <= length ts,
        may be a redex. Example: map (\<lambda>x. x) = (\<lambda>xs. xs) wrt map_cong*)
                            (let
                               val thm = congc (prover ctxt) ctxt maxidx cong t0;
                               val t = the_default t0 (Option.map Thm.rhs_of thm);
                               val (cl, cr) = Thm.dest_comb t
                               val dVar = Var(("", 0), dummyT)
                               val skel =
                                 list_comb (h, replicate (length ts) dVar)
                             in
                               (case botc skel ctxt cl of
                                 NONE => thm
                               | SOME thm' =>
                                   transitive3 thm (Thm.combination thm' (Thm.reflexive cr)))
                             end handle Pattern.MATCH => appc ()))
                      | _ => appc ())
                   end)
             | _ => NONE)
         end
     and impc ct ctxt =
       if mutsimp then mut_impc0 [] ct [] [] ctxt
       else nonmut_impc ct ctxt
 
     and rules_of_prem prem ctxt =
       if maxidx_of_term (Thm.term_of prem) <> ~1
       then
        (cond_tracing ctxt (fn () =>
           print_term ctxt "Cannot add premise as rewrite rule because it contains (type) unknowns:"
             (Thm.term_of prem));
         (([], NONE), ctxt))
       else
         let val (asm, ctxt') = Thm.assume_hyps prem ctxt
         in ((extract_safe_rrules ctxt' asm, SOME asm), ctxt') end
 
     and add_rrules (rrss, asms) ctxt =
       (fold o fold) insert_rrule rrss ctxt |> add_prems (map_filter I asms)
 
     and disch r prem eq =
       let
         val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
         val eq' =
           Thm.implies_elim
             (Thm.instantiate (TVars.empty, Vars.make3 (vA, prem) (vB, lhs) (vC, rhs))
               Drule.imp_cong)
             (Thm.implies_intr prem eq);
       in
         if not r then eq'
         else
           let
             val (prem', concl) = Thm.dest_implies lhs;
             val (prem'', _) = Thm.dest_implies rhs;
           in
             Thm.transitive
               (Thm.transitive
                 (Thm.instantiate (TVars.empty, Vars.make3 (vA, prem') (vB, prem) (vC, concl))
                   Drule.swap_prems_eq)
                 eq')
               (Thm.instantiate (TVars.empty, Vars.make3 (vA, prem) (vB, prem'') (vC, concl))
                 Drule.swap_prems_eq)
           end
       end
 
     and rebuild [] _ _ _ _ eq = eq
       | rebuild (prem :: prems) concl (_ :: rrss) (_ :: asms) ctxt eq =
           let
             val ctxt' = add_rrules (rev rrss, rev asms) ctxt;
             val concl' =
               Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq));
             val dprem = Option.map (disch false prem);
           in
             (case rewritec (prover, maxidx) ctxt' concl' of
               NONE => rebuild prems concl' rrss asms ctxt (dprem eq)
             | SOME (eq', _) =>
                 transitive2 (fold (disch false) prems (the (transitive3 (dprem eq) eq')))
                   (mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ctxt))
           end
 
     and mut_impc0 prems concl rrss asms ctxt =
       let
         val prems' = strip_imp_prems concl;
         val ((rrss', asms'), ctxt') = fold_map rules_of_prem prems' ctxt |>> split_list;
       in
         mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss')
           (asms @ asms') [] [] [] [] ctxt' ~1 ~1
       end
 
     and mut_impc [] concl [] [] prems' rrss' asms' eqns ctxt changed k =
         transitive1 (fold (fn (eq1, prem) => fn eq2 => transitive1 eq1
             (Option.map (disch false prem) eq2)) (eqns ~~ prems') NONE)
           (if changed > 0 then
              mut_impc (rev prems') concl (rev rrss') (rev asms')
                [] [] [] [] ctxt ~1 changed
            else rebuild prems' concl rrss' asms' ctxt
              (botc skel0 (add_rrules (rev rrss', rev asms') ctxt) concl))
 
       | mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms)
           prems' rrss' asms' eqns ctxt changed k =
         (case (if k = 0 then NONE else botc skel0 (add_rrules
           (rev rrss' @ rrss, rev asms' @ asms) ctxt) prem) of
             NONE => mut_impc prems concl rrss asms (prem :: prems')
               (rrs :: rrss') (asm :: asms') (NONE :: eqns) ctxt changed
               (if k = 0 then 0 else k - 1)
         | SOME eqn =>
             let
               val prem' = Thm.rhs_of eqn;
               val tprems = map Thm.term_of prems;
               val i = 1 + fold Integer.max (map (fn p =>
                 find_index (fn q => q aconv p) tprems) (Thm.hyps_of eqn)) ~1;
               val ((rrs', asm'), ctxt') = rules_of_prem prem' ctxt;
             in
               mut_impc prems concl rrss asms (prem' :: prems')
                 (rrs' :: rrss') (asm' :: asms')
                 (SOME (fold_rev (disch true)
                   (take i prems)
                   (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies
                     (drop i prems, concl))))) :: eqns)
                 ctxt' (length prems') ~1
             end)
 
     (*legacy code -- only for backwards compatibility*)
     and nonmut_impc ct ctxt =
       let
         val (prem, conc) = Thm.dest_implies ct;
         val thm1 = if simprem then botc skel0 ctxt prem else NONE;
         val prem1 = the_default prem (Option.map Thm.rhs_of thm1);
         val ctxt1 =
           if not useprem then ctxt
           else
             let val ((rrs, asm), ctxt') = rules_of_prem prem1 ctxt
             in add_rrules ([rrs], [asm]) ctxt' end;
       in
         (case botc skel0 ctxt1 conc of
           NONE =>
             (case thm1 of
               NONE => NONE
             | SOME thm1' => SOME (Drule.imp_cong_rule thm1' (Thm.reflexive conc)))
         | SOME thm2 =>
             let val thm2' = disch false prem1 thm2 in
               (case thm1 of
                 NONE => SOME thm2'
               | SOME thm1' =>
                  SOME (Thm.transitive (Drule.imp_cong_rule thm1' (Thm.reflexive conc)) thm2'))
             end)
       end;
 
   in try_botc end;
 
 
 (* Meta-rewriting: rewrites t to u and returns the theorem t \<equiv> u *)
 
 (*
   Parameters:
     mode = (simplify A,
             use A in simplifying B,
             use prems of B (if B is again a meta-impl.) to simplify A)
            when simplifying A \<Longrightarrow> B
     prover: how to solve premises in conditional rewrites and congruences
 *)
 
 fun rewrite_cterm mode prover raw_ctxt raw_ct =
   let
     val thy = Proof_Context.theory_of raw_ctxt;
 
     val ct = raw_ct
       |> Thm.transfer_cterm thy
       |> Thm.adjust_maxidx_cterm ~1;
     val maxidx = Thm.maxidx_of_cterm ct;
 
     val ctxt =
       raw_ctxt
       |> Variable.set_body true
       |> Context_Position.set_visible false
       |> inc_simp_depth
       |> (fn ctxt => trace_invoke {depth = simp_depth ctxt, term = Thm.term_of ct} ctxt);
 
     val _ =
       cond_tracing ctxt (fn () =>
         print_term ctxt "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" (Thm.term_of ct));
   in
     ct
     |> bottomc (mode, Option.map (Drule.flexflex_unique (SOME ctxt)) oo prover, maxidx) ctxt
     |> Thm.solve_constraints
   end;
 
 val simple_prover =
   SINGLE o (fn ctxt => ALLGOALS (resolve_tac ctxt (prems_of ctxt)));
 
 fun rewrite _ _ [] = Thm.reflexive
   | rewrite ctxt full thms =
       rewrite_cterm (full, false, false) simple_prover (init_simpset thms ctxt);
 
 fun rewrite_rule ctxt = Conv.fconv_rule o rewrite ctxt true;
 
 (*simple term rewriting -- no proof*)
 fun rewrite_term thy rules procs =
   Pattern.rewrite_term thy (map decomp_simp' rules) procs;
 
 fun rewrite_thm mode prover ctxt = Conv.fconv_rule (rewrite_cterm mode prover ctxt);
 
 (*Rewrite the subgoals of a proof state (represented by a theorem)*)
 fun rewrite_goals_rule ctxt thms th =
   Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
     (init_simpset thms ctxt))) th;
 
 
 (** meta-rewriting tactics **)
 
 (*Rewrite all subgoals*)
 fun rewrite_goals_tac ctxt defs = PRIMITIVE (rewrite_goals_rule ctxt defs);
 
 (*Rewrite one subgoal*)
 fun generic_rewrite_goal_tac mode prover_tac ctxt i thm =
   if 0 < i andalso i <= Thm.nprems_of thm then
     Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ctxt) i thm)
   else Seq.empty;
 
 fun rewrite_goal_tac ctxt thms =
   generic_rewrite_goal_tac (true, false, false) (K no_tac) (init_simpset thms ctxt);
 
 (*Prunes all redundant parameters from the proof state by rewriting.*)
 fun prune_params_tac ctxt = rewrite_goals_tac ctxt [Drule.triv_forall_equality];
 
 
 (* for folding definitions, handling critical pairs *)
 
 (*The depth of nesting in a term*)
 fun term_depth (Abs (_, _, t)) = 1 + term_depth t
   | term_depth (f $ t) = 1 + Int.max (term_depth f, term_depth t)
   | term_depth _ = 0;
 
 val lhs_of_thm = #1 o Logic.dest_equals o Thm.prop_of;
 
 (*folding should handle critical pairs!  E.g. K \<equiv> Inl 0,  S \<equiv> Inr (Inl 0)
   Returns longest lhs first to avoid folding its subexpressions.*)
 fun sort_lhs_depths defs =
   let val keylist = AList.make (term_depth o lhs_of_thm) defs
       val keys = sort_distinct (rev_order o int_ord) (map #2 keylist)
   in map (AList.find (op =) keylist) keys end;
 
 val rev_defs = sort_lhs_depths o map Thm.symmetric;
 
 fun fold_rule ctxt defs = fold (rewrite_rule ctxt) (rev_defs defs);
 fun fold_goals_tac ctxt defs = EVERY (map (rewrite_goals_tac ctxt) (rev_defs defs));
 
 
 (* HHF normal form: \<And> before \<Longrightarrow>, outermost \<And> generalized *)
 
 local
 
 fun gen_norm_hhf protect ss ctxt0 th0 =
   let
     val (ctxt, th) = Thm.join_transfer_context (ctxt0, th0);
     val th' =
       if Drule.is_norm_hhf protect (Thm.prop_of th) then th
       else
         Conv.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th;
   in th' |> Thm.adjust_maxidx_thm ~1 |> Variable.gen_all ctxt end;
 
 val hhf_ss =
   Context.the_local_context ()
   |> init_simpset Drule.norm_hhf_eqs
   |> simpset_of;
 
 val hhf_protect_ss =
   Context.the_local_context ()
   |> init_simpset Drule.norm_hhf_eqs
   |> add_eqcong Drule.protect_cong
   |> simpset_of;
 
 in
 
 val norm_hhf = gen_norm_hhf {protect = false} hhf_ss;
 val norm_hhf_protect = gen_norm_hhf {protect = true} hhf_protect_ss;
 
-fun norm_hhf_protect_without_context th =
-  norm_hhf_protect (Proof_Context.init_global (Thm.theory_of_thm th)) th;
-
 end;
 
 end;
 
 structure Basic_Meta_Simplifier: BASIC_RAW_SIMPLIFIER = Raw_Simplifier;
 open Basic_Meta_Simplifier;