diff --git a/thys/ML_Unification/ML_Utils/General/general_util.ML b/thys/ML_Unification/ML_Utils/General/general_util.ML
--- a/thys/ML_Unification/ML_Utils/General/general_util.ML
+++ b/thys/ML_Unification/ML_Utils/General/general_util.ML
@@ -1,67 +1,74 @@
 (*  Title:      ML_Utils/general_util.ML
     Author:     Kevin Kappelmann
 
 General ML utilities.
 *)
 signature GENERAL_UTIL =
 sig
   val flip : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
 
   val find_first_index : ('a -> bool) -> 'a list -> (int * 'a) option
+  val find_indices : ('a -> bool) -> 'a list -> int list
 
   (*returns false if function throws an exception*)
   val try_bool : ('a -> bool) -> 'a -> bool
 
   (*lists*)
   val fold_rev_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
 
   (* sequences *)
   (*raises exception if sequence is empty and returns the sequence otherwise*)
   val seq_try : exn -> 'a Seq.seq -> 'a Seq.seq
   val seq_is_empty : 'a Seq.seq -> (bool * 'a Seq.seq)
   val seq_merge : 'a ord -> ('a Seq.seq * 'a Seq.seq) -> 'a Seq.seq
 
 end
 
 structure General_Util : GENERAL_UTIL =
 struct
 
 fun flip f x y = f y x
 
 fun find_first_index p = get_index (Option.filter p)
 
+fun find_indices p =
+  let
+    fun find_indices _ [] = []
+      | find_indices i (x :: xs) = (p x ? cons i) (find_indices (i + 1) xs)
+  in find_indices 0 end
+
 fun try_bool f = try f #> (Option.getOpt o rpair false)
 
 (*lists*)
 fun insert _ x [] = [x]
   | insert ord x (y :: ys) = case ord (x, y) of
       LESS => x :: y :: ys
     | EQUAL => x :: y :: ys
     | GREATER => y :: insert ord x ys
 
 fun fold_rev_index f =
   let fun fold_aux _ [] y = y
         | fold_aux i (x :: xs) y = f (i, x) (fold_aux (i + 1) xs y)
   in fold_aux 0 end
 
 (* sequences *)
 fun seq_try exn sq = case Seq.pull sq of
     NONE => raise exn
   | SOME v => Seq.make (fn () => SOME v)
 
 fun seq_is_empty sq = case Seq.pull sq of
     NONE => (true, Seq.empty)
   | SOME v => (false, Seq.make (fn () => SOME v))
 
 fun seq_merge ord (xq, yq) =
   Seq.make (fn () => (case Seq.pull xq of
       NONE => Seq.pull yq
     | SOME (x, xq') => case Seq.pull yq of
         NONE => Seq.pull xq
       | SOME (y, yq') => case ord (x, y) of
           LESS => SOME (x, seq_merge ord (xq', Seq.cons y yq'))
         | EQUAL => SOME (x, seq_merge ord (xq', Seq.cons y yq'))
         | GREATER => SOME (y, seq_merge ord (Seq.cons x xq', yq')))
   )
 
 end
\ No newline at end of file
diff --git a/thys/ML_Unification/ML_Utils/Parsing/parse_key_value.ML b/thys/ML_Unification/ML_Utils/Parsing/parse_key_value.ML
--- a/thys/ML_Unification/ML_Utils/Parsing/parse_key_value.ML
+++ b/thys/ML_Unification/ML_Utils/Parsing/parse_key_value.ML
@@ -1,81 +1,81 @@
 (*  Title:      ML_Utils/parse_key_value.ML
     Author:     Kevin Kappelmann
 
 Parsing of key-value pairs.
 *)
 signature PARSE_KEY_VALUE =
 sig
   type ('k, 'v) entry = ('k * 'v)
   type ('k, 'v) entries = ('k, 'v) entry list
 
   (*takes key parser, delimiter parser, value parser*)
   val parse_entry : 'k parser -> 'd parser -> ('k -> 'v parser) -> (('k, 'v) entry) parser
   val parse_entry' : 'k context_parser -> 'd context_parser -> ('k -> 'v context_parser) ->
     (('k, 'v) entry) context_parser
 
   val pretty_keys : ('k -> string) -> 'k list -> Pretty.T
   val parse_key : string list -> (string -> 'k) -> 'k parser
 
   val has_required_keys : ('k * ('k, 'v) entry -> bool) -> 'k list -> ('k, 'v) entries -> bool
 
   val parse_entries_required : ('k * 'k -> bool) -> ('k -> string) -> 'k list ->
     (('k, 'v) entries) parser -> (('k, 'v) entries) parser
   val parse_entries_required' : ('k * 'k -> bool) -> ('k -> string) -> 'k list ->
     (('k, 'v) entries) context_parser -> (('k, 'v) entries) context_parser
 end
 
 structure Parse_Key_Value : PARSE_KEY_VALUE =
 struct
 
 structure Util = Parse_Util
 
 type ('k, 'v) entry = ('k * 'v)
 type ('k, 'v) entries = ('k, 'v) entry list
 
 fun gen_parse_entry cut parse_key parse_delim parse_value =
   parse_key
   :-- (fn n => parse_delim
   |-- cut (parse_value n))
 fun parse_entry parse_key = gen_parse_entry Parse.!!! parse_key
-fun parse_entry' parse_key = gen_parse_entry Util.!!!+ parse_key
+fun parse_entry' parse_key = gen_parse_entry Parse.!!!! parse_key
 
 fun pretty_keys key_to_string = map (Pretty.str o key_to_string) #> Pretty.commas #> Pretty.block
 
 fun parse_key names key_from_string =
   let val pretty_keys = pretty_keys I names |> Pretty.string_of
   in
     Parse.group (K pretty_keys)
       (Util.nonempty_name (K "Key must not be empty.") >> key_from_string)
   end
 
 fun eq_key_entry eq_key (rn, (xn, _)) = eq_key (rn, xn)
 
 fun has_required_keys eq_key_entry rks ks = subset eq_key_entry (rks, ks)
 
 fun gen_parse_entries_required filter_parser eq_key key_to_string ks parse_entries =
   let
     val eq_key_entry = eq_key_entry eq_key
     fun failure_required es = Pretty.fbreaks [
         Pretty.block [
           Pretty.str "Missing keys: ",
           pretty_keys key_to_string (subtract (eq_key_entry o swap) es ks)
         ],
         Pretty.block [
           Pretty.str "Required keys: ",
           pretty_keys key_to_string ks
         ]
       ] |> Pretty.block |> Pretty.string_of
     fun failure_distinct es _ = Pretty.block [
         Pretty.str "All keys must be distinct. Duplicates: ",
         duplicates eq_key (map fst es) |> pretty_keys key_to_string
       ] |> Pretty.string_of
   in
     filter_parser
       (has_required_keys eq_key_entry ks) (Util.fail failure_required) parse_entries
     |> Util.distinct_list (eq_key o apply2 fst) failure_distinct
   end
 
 fun parse_entries_required eq_key = gen_parse_entries_required Util.filter_cut eq_key
 fun parse_entries_required' eq_key = gen_parse_entries_required Util.filter_cut' eq_key
 
 end
\ No newline at end of file
diff --git a/thys/ML_Unification/ML_Utils/Parsing/parse_util.ML b/thys/ML_Unification/ML_Utils/Parsing/parse_util.ML
--- a/thys/ML_Unification/ML_Utils/Parsing/parse_util.ML
+++ b/thys/ML_Unification/ML_Utils/Parsing/parse_util.ML
@@ -1,167 +1,137 @@
 (*  Title:      ML_Utils/util.ML
     Author:     Kevin Kappelmann
 
 Parsing utilities.
 *)
 signature PARSE_UTIL =
 sig
-  (*cut for context parsers*)
-  val !!!+ : 'a context_parser -> 'a context_parser
-
-  val enum1' : string -> 'a context_parser -> 'a list context_parser
-  val enum' : string -> 'a context_parser -> 'a list context_parser
-  val and_list1' : 'a context_parser -> 'a list context_parser
-  val and_list' : 'a context_parser -> 'a list context_parser
-
   (*indexed state monad (generalising parsers and context parsers)*)
   type ('i, 'j, 'a) istate = 'i -> 'a * 'j
 
   (*"if_ahead p1 f p2" applies f to result of p1 if p1 is successful; otherwise runs p2*)
   val if_ahead : ('a, 'b, 'c) istate -> ('c -> 'a -> 'd) -> ('a, 'a, 'd) istate ->
     ('a, 'a, 'd) istate
 
   (*if_ahead applied to end-of-file parser*)
   val if_eof : (string -> Token.T list -> 'a) -> 'a parser -> 'a parser
   val if_eof' : (string -> Context.generic * Token.T list -> 'a) -> 'a context_parser ->
     'a context_parser
 
   val option : 'a parser -> ('a option) parser
   val option' : 'a context_parser -> ('a option) context_parser
   val optional : 'a parser -> 'a -> 'a parser
   val optional' : 'a context_parser -> 'a -> 'a context_parser
 
   val position : 'a parser -> ('a * Position.T) parser
   val position' : 'a context_parser -> ('a * Position.T) context_parser
 
   val fail : ('a -> string) -> 'a -> 'b
   (*scanner raising Scan.ABORT with given error message*)
   val abort : (Token.T list -> string) -> 'a parser
   val abort' : (Context.generic * Token.T list -> string) -> 'a context_parser
 
   (*"filter f err p" runs parser p to obtain result x and returns x if "f x" holds and "err x" otherwise*)
   val filter : ('a -> bool) -> ('a -> ('b, 'b, 'a) istate) -> ('c, 'b, 'a) istate ->
     ('c, 'b, 'a) istate
   (*filter with cuts in case of failure*)
   val filter_cut : ('a -> bool) -> ('a -> Token.T list -> string) -> 'a parser -> 'a parser
   val filter_cut' : ('a -> bool) -> ('a -> Context.generic * Token.T list -> string) ->
     'a context_parser -> 'a context_parser
 
   val nonempty_list : ('b -> string) -> ('a, 'b, 'c list) istate -> ('a, 'b, 'c list) istate
   val distinct_list : ('a * 'a -> bool) -> ('a list -> 'c -> string) -> ('b, 'c, 'a list) istate ->
     ('b, 'c, 'a list) istate
 
   val nonempty_name : (Token.T list -> string) -> string parser
 
   val code : ML_Code_Util.code parser
   val nonempty_code : (Token.T list -> string) -> ML_Code_Util.code parser
 
   val bool : bool parser
   val eq : string parser
   val parenths : 'a parser -> 'a parser
   val parenths' : 'a context_parser -> 'a context_parser
 
   val thm : thm context_parser
   val multi_thm : (thm list) context_parser
   val thms : (thm list) context_parser
   val nonempty_thms : (Context.generic * Token.T list -> string) -> (thm list) context_parser
 
   (*the following structure may be ignored; it is needed for below ML_int parser*)
   structure Internal_Int_Data : GENERIC_DATA
   val ML_int : (Token.T list -> string) -> int context_parser
 end
 
 structure Parse_Util : PARSE_UTIL =
 struct
 
-(*FIXME: move to Isabelle kernel?*)
-fun get_tokens_pos [] = " (end-of-input)"
-  | get_tokens_pos (tok :: _) = Position.here (Token.pos_of tok);
-
-fun cut get_pos kind scan =
-  let
-    fun err (x, NONE) = (fn () => kind ^ get_pos x)
-      | err (x, SOME msg) =
-          (fn () =>
-            let val s = msg () in
-              if String.isPrefix kind s then s
-              else kind ^ get_pos x ^ ": " ^ s
-            end);
-  in Scan.!! err scan end;
-
-fun !!!+ scan = cut (get_tokens_pos o snd) "Outer syntax error" scan
-
-fun enum1' sep scan = scan ::: Scan.repeat (Scan.lift (Parse.$$$ sep) |-- !!!+ scan);
-fun enum' sep scan = enum1' sep scan || Scan.succeed [];
-fun and_list1' scan = enum1' "and" scan;
-fun and_list' scan = enum' "and" scan;
-
 type ('i, 'j, 'a) istate = 'i -> 'a * 'j
 
 fun if_ahead ahead f scan =
   (Scan.ahead ahead :|-- (fn st => fn xs => (f st xs, xs))) || scan
 
 fun if_eof scan = if_ahead Parse.eof scan
 fun if_eof' scan = if_ahead (Scan.lift Parse.eof) scan
 
 fun option scan = if_eof (K o K NONE) (Scan.option scan)
 fun option' scan = if_eof' (K o K NONE) (Scan.option scan)
 fun optional scan default = option scan >> the_default default
 fun optional' scan default = option' scan >> the_default default
 
 fun gen_position not_eof scan =
   (Scan.optional (Scan.ahead not_eof >> Token.pos_of) Position.none
   >> (snd o Position.default))
   -- scan
   >> swap
 
 fun position scan = gen_position Parse.not_eof scan
 fun position' scan = gen_position (Scan.lift Parse.not_eof) scan
 
 fun fail msg_of = Scan.fail_with (fn x => fn _ => msg_of x)
 fun gen_abort cut msg_of = fail msg_of |> cut
 
 fun abort msg_of = gen_abort Parse.!!! msg_of
-fun abort' msg_of = gen_abort !!!+ msg_of
+fun abort' msg_of = gen_abort Parse.!!!! msg_of
 
 fun filter p err scan = scan :|-- (fn x => if p x then pair x else err x)
 fun gen_filter_cut abort p msg_of = filter p (abort o msg_of)
 fun filter_cut p = gen_filter_cut abort p
 fun filter_cut' p = gen_filter_cut abort' p
 
 fun nonempty_list msg_of = filter (not o null) (K (fail msg_of))
 fun distinct_list eq msg_of = filter (not o has_duplicates eq) (fail o msg_of)
 fun nonempty_name msg_of = filter (curry (op <>) "") (K (fail msg_of)) Args.name
 
 val code = if_eof (K o K []) ML_Code_Util.parse_code
 fun nonempty_code msg_of = nonempty_list msg_of code
 
 val bool = Scan.recover (Args.name >> Value.parse_bool)
   (fail (K "expected \"true\" or \"false\""))
 
 val eq = Parse.$$$ "\<equiv>" || Parse.$$$ "=" || fail (K "expected \"=\" or \"\<equiv>\"")
 
 fun parenths scan = Parse.$$$ "(" |-- scan --| Parse.$$$ ")"
 fun parenths' scan = (Scan.lift (Parse.$$$ "(")) |-- scan --| (Scan.lift (Parse.$$$ ")"))
 
 (*for better error messages than Attrib.thm and friends*)
 fun thm x = Attrib.thm x handle ERROR m => fail (K m) ()
 fun multi_thm x = Attrib.multi_thm x handle ERROR m => fail (K m) ()
 val thms = Scan.repeats multi_thm
 fun nonempty_thms msg_of = nonempty_list msg_of thms
 
 structure Internal_Int_Data = Generic_Data( type T = int val empty = 0 val merge = fst)
 
 fun ML_int msg_of =
   let fun int_from_code ((code, ctxt), pos) =
     let val put_int_code = ML_Code_Util.read "Parse_Util.Internal_Int_Data.put"
       @ ML_Code_Util.atomic code
     in
       Context.Proof ctxt
       |> ML_Attribute_Util.attribute_map_context (ML_Attribute.run_map_context (put_int_code, pos))
       |> Internal_Int_Data.get
     end
   in
     Scan.lift Parse.int
     || ((Scan.lift (nonempty_code msg_of) -- Args.context |> position') >> int_from_code)
   end
 end
diff --git a/thys/ML_Unification/ML_Utils/Tactics/tactic_util.ML b/thys/ML_Unification/ML_Utils/Tactics/tactic_util.ML
--- a/thys/ML_Unification/ML_Utils/Tactics/tactic_util.ML
+++ b/thys/ML_Unification/ML_Utils/Tactics/tactic_util.ML
@@ -1,234 +1,234 @@
 (*  Title:      ML_Utils/tactic_util.ML
     Author:     Kevin Kappelmann
 
 Tactic utilities.
 *)
 signature TACTIC_UTIL =
 sig
   include HAS_LOGGER
   (* tactic combinators*)
   val HEADGOAL : (int -> 'a) -> 'a
 
   val TRY' : ('a -> tactic) -> 'a -> tactic
 
   val EVERY_ARG : ('a -> tactic) -> 'a list -> tactic
   val EVERY_ARG' : ('a -> 'b -> tactic) -> 'a list -> 'b -> tactic
   val CONCAT : tactic list -> tactic
   val CONCAT' : ('a -> tactic) list -> 'a -> tactic
 
   val FOCUS_PARAMS' : (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic
   val FOCUS_PARAMS_CTXT : (Proof.context -> tactic) -> Proof.context -> int -> tactic
   val FOCUS_PARAMS_CTXT' : (Proof.context -> int -> tactic) -> Proof.context -> int -> tactic
   val FOCUS_PARAMS_FIXED' : (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic
   val FOCUS_PREMS' : (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic
   val FOCUS' : (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic
   val SUBPROOF' : (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic
 
   val CSUBGOAL_DATA : (cterm -> 'a) -> ('a -> int -> tactic) -> int -> tactic
   val CSUBGOAL_STRIPPED : (cterm Binders.binders * (cterm list * cterm) -> 'a) ->
     ('a -> int -> tactic) -> int -> tactic
   val SUBGOAL_DATA : (term -> 'a) -> ('a -> int -> tactic) -> int -> tactic
   val SUBGOAL_STRIPPED : ((string * typ) list * (term list * term) -> 'a) ->
     ('a -> int -> tactic) -> int -> tactic
 
   (* tactics *)
   val insert_tac : thm list -> Proof.context -> int -> tactic
   (*thin_tac n i deletes nth premise of the ith subgoal*)
   val thin_tac : int -> int -> tactic
   val thin_tacs : int list -> int -> tactic
 
   val safe_simp_tac : Proof.context -> int -> tactic
 
   (*nth_eq_assume_tac n i solves ith subgoal by assumption, without unification,
     preferring premise n*)
   val nth_eq_assume_tac : int -> int -> tactic
 
   (*resolution with matching and without lifting of premises and parameters*)
   val no_lift_biresolve_tac : bool -> thm -> int -> Proof.context -> int -> tactic
   val no_lift_resolve_tac : thm -> int -> Proof.context -> int -> tactic
   val no_lift_eresolve_tac : thm -> int -> Proof.context -> int -> tactic
 
   (*rewrite subgoal according to the given equality theorem "lhs \<equiv> subgoal"*)
   val rewrite_subgoal_tac : thm -> Proof.context -> int -> tactic
 
   (*creates equality theorem for a subgoal from an equality theorem for the subgoal's conclusion*)
   val eq_subgoal_from_eq_concl : cterm Binders.binders -> cterm list -> thm -> Proof.context -> thm
 
   (*rewrite a subgoal given an equality theorem and environment for the subgoal's conclusion*)
   val rewrite_subgoal_unif_concl : Envir_Normalisation.thm_normaliser ->
     Envir_Normalisation.thm_normaliser -> term Binders.binders -> (Envir.env * thm) ->
     Proof.context -> int -> tactic
 
   (*protect premises starting from (and excluding) the given index in the specified subgoal*)
   val protect_tac : int -> Proof.context -> int -> tactic
   (*unprotect the subgoal*)
   val unprotect_tac : Proof.context -> int -> tactic
   (*protect, then apply tactic, then unprotect*)
   val protected_tac : int -> (int -> tactic) -> Proof.context -> int -> tactic
 
   (*focus on the specified subgoal, introducing only the specified list of premises
     as theorems in the focus*)
   val focus_prems_tac : int list -> (Subgoal.focus -> int -> tactic) ->
     Proof.context -> int -> tactic
   (*focus_prems_tac and then deletes all focused premises*)
   val focus_delete_prems_tac : int list -> (Subgoal.focus -> int -> tactic) ->
     Proof.context -> int -> tactic
 
   (*apply tactic to the specified subgoal, where the state is given as a cterm*)
   val apply_tac : (int -> tactic) -> int -> cterm -> thm Seq.seq
 
 end
 
 structure Tactic_Util : TACTIC_UTIL =
 struct
 
 val logger = Logger.setup_new_logger Logger.root_logger "Tactic_Util"
 
 (* tactic combinators *)
 fun HEADGOAL f = f 1
 
 fun TRY' tac =  tac ORELSE' K all_tac
 
 fun EVERY_ARG tac = EVERY o map tac
 fun EVERY_ARG' tac = EVERY' o map tac
 
 fun CONCAT tacs = fold_rev (curry op APPEND) tacs no_tac
 fun CONCAT' tacs = fold_rev (curry op APPEND') tacs (K no_tac)
 
 fun FOCUS_PARAMS' tac = Subgoal.FOCUS_PARAMS (HEADGOAL o tac)
 fun FOCUS_PARAMS_FIXED' tac = Subgoal.FOCUS_PARAMS_FIXED (HEADGOAL o tac)
 fun FOCUS_PREMS' tac = Subgoal.FOCUS_PREMS (HEADGOAL o tac)
 fun FOCUS' tac = Subgoal.FOCUS (HEADGOAL o tac)
 fun SUBPROOF' tac = Subgoal.SUBPROOF (HEADGOAL o tac)
 
 fun FOCUS_PARAMS_CTXT tac = Subgoal.FOCUS_PARAMS (#context #> tac)
 fun FOCUS_PARAMS_CTXT' tac = FOCUS_PARAMS' (#context #> tac)
 
 fun CSUBGOAL_DATA f tac = CSUBGOAL (uncurry tac o apfst f)
 fun CSUBGOAL_STRIPPED f = CSUBGOAL_DATA (f o Term_Util.strip_csubgoal)
 fun SUBGOAL_DATA f tac = SUBGOAL (uncurry tac o apfst f)
 fun SUBGOAL_STRIPPED f = SUBGOAL_DATA (f o Term_Util.strip_subgoal)
 
 (* tactics *)
 fun insert_tac thms ctxt = Method.insert_tac ctxt thms
 
 fun thin_tac n = if n < 1 then K no_tac
   else rotate_tac (n - 1) THEN' (DETERM o eresolve0_tac [thin_rl]) THEN' rotate_tac (~n + 1)
 val thin_tacs = sort int_ord
   #> map_index ((op -) o swap)
   #> EVERY_ARG' thin_tac
 
 (*some "safe" solvers create instantiations via flex-flex pairs, which we disallow here*)
 fun safe_simp_tac ctxt i state =
   let val eq_flexps = Thm.tpairs_of
     #> pair (Thm.tpairs_of state)
     #> eq_list (eq_pair (op aconv) (op aconv))
   in Simplifier.safe_simp_tac ctxt i state |> Seq.filter eq_flexps end
 
 fun nth_eq_assume_tac n = if n < 1 then K no_tac
   else rotate_tac (n - 1) THEN' eq_assume_tac
 
 (*resolution*)
 fun no_lift_biresolve_tac eres brule nsubgoals ctxt =
   Thm.bicompose (SOME ctxt) {flatten = true, match = true, incremented = true}
   (eres, brule, nsubgoals)
   #> PRIMSEQ
 
 val no_lift_resolve_tac = no_lift_biresolve_tac false
 val no_lift_eresolve_tac = no_lift_biresolve_tac true
 
 fun rewrite_subgoal_tac eq_thm =
   let
     val (lhs, rhs) = Thm.dest_equals (Thm.cconcl_of eq_thm)
     val eq_elim = Thm.instantiate' [] [SOME lhs, SOME rhs] Drule.equal_elim_rule1
     val thm = Thm.implies_elim eq_elim eq_thm
   in no_lift_resolve_tac thm 1 end
 
 fun eq_subgoal_from_eq_concl cbinders cprems eq_thm ctxt =
   let
     fun all_abstract ((x, T), cfree) =
       let val all_const = Logic.all_const T |> Thm.cterm_of ctxt
       in
         Thm.abstract_rule x cfree
         #> Drule.arg_cong_rule all_const
       end
   in
     (*introduce the premises*)
     fold_rev (Drule.imp_cong_rule o Thm.reflexive) cprems eq_thm
     (*introduce abstractions for the fresh Frees*)
     |> fold all_abstract cbinders
   end
 
 fun rewrite_subgoal_unif_concl norm_state norm_eq_thm binders (env, eq_thm) ctxt i state =
   let
     fun rewrite_tac (rparams, (prems, _)) =
       let
         (*update binders with their normalised type*)
         val binders = map2 (fn (_, T) => fn ((n, _), Free (n', _)) => ((n, T), Free (n', T)))
           rparams binders
         val cterm_of = Thm.cterm_of ctxt
         val cprems = map (cterm_of o Binders.replace_binders binders) prems
         val eq_thm = eq_subgoal_from_eq_concl (map (apsnd cterm_of) binders) cprems
           (norm_eq_thm ctxt env eq_thm) ctxt
       in rewrite_subgoal_tac eq_thm ctxt end
   in
     ((PRIMITIVE (norm_state ctxt env) |> K)
     THEN' SUBGOAL_STRIPPED I rewrite_tac) i state
   end
 
 fun protect_tac n ctxt =
   let fun protect cbinders (cprems, cconcl) i =
     let val nprems = length cprems
     in
       if nprems < n then
         (@{log Logger.WARN} ctxt (fn _ => Pretty.block [
           Pretty.str "Not enough premises to protect. Given number: ",
           Pretty.str (string_of_int n),
           Pretty.str ". But there are only ",
           Pretty.str (string_of_int nprems),
           Pretty.str " premise(s) in subgoal ",
           Pretty.str (string_of_int i),
           Pretty.str ": ",
           Logic.close_prop (map (apfst fst o apsnd Thm.term_of) cbinders) (map Thm.term_of cprems)
             (Thm.term_of cconcl) |> Syntax.pretty_term ctxt
         ] |> Pretty.string_of);
         no_tac)
       else
         let
           val (cprems_unprotected, cconcl_protected) = chop n cprems
             ||> Drule.list_implies o rpair cconcl
           val protected_eq_thm = @{thm Pure.prop_def}
             |> Thm.instantiate' [] [SOME cconcl_protected]
             |> (fn eq_thm => eq_subgoal_from_eq_concl cbinders cprems_unprotected eq_thm ctxt)
         in rewrite_subgoal_tac protected_eq_thm ctxt i end
     end
   in if n < 0 then K no_tac else CSUBGOAL_STRIPPED I (uncurry protect) end
 
 fun unprotect_tac ctxt = match_tac ctxt [Drule.protectI]
 
 fun protected_tac n tac ctxt =
   protect_tac n ctxt
   THEN' tac
   THEN_ALL_NEW (unprotect_tac ctxt)
 
 fun focus_prems_tac is tac ctxt =
   CONVERSION (Conversion_Util.move_prems_to_front_conv is)
   THEN' protect_tac (length is) ctxt
-  THEN' FOCUS' (fn {context=ctxt, params=params, prems=prems,
+  THEN' FOCUS_PREMS' (fn {context=ctxt, params=params, prems=prems,
     asms=asms, concl=concl, schematics=schematics} =>
     let val concl = Term_Util.unprotect concl
     in
       unprotect_tac ctxt
       THEN' tac {context=ctxt, params=params, prems=prems, asms=asms, concl=concl,
         schematics=schematics}
     end
   ) ctxt
 
 fun focus_delete_prems_tac is tac ctxt =
   focus_prems_tac is tac ctxt
   THEN' thin_tacs (1 upto length is)
 
 fun apply_tac tac i = Goal.init #> tac i #> Seq.map Goal.conclude
 
 end
 
diff --git a/thys/ML_Unification/Unification_Hints/term_index_unification_hints.ML b/thys/ML_Unification/Unification_Hints/term_index_unification_hints.ML
--- a/thys/ML_Unification/Unification_Hints/term_index_unification_hints.ML
+++ b/thys/ML_Unification/Unification_Hints/term_index_unification_hints.ML
@@ -1,381 +1,381 @@
 (*  Title:      ML_Unification/term_index_unification_hints.ML
     Author:     Kevin Kappelmann
 
 Unification hints stored in a term index.
 *)
 @{parse_entries (sig) PARSE_TERM_INDEX_UNIFICATION_HINTS_MODE
   [add, del]}
 
 @{parse_entries (sig) PARSE_TERM_INDEX_UNIFICATION_HINTS_ARGS
   [concl_unifier, normalisers, prems_unifier, retrieval, hint_preprocessor, prio]}
 
 @{parse_entries (sig) PARSE_TERM_INDEX_UNIFICATION_HINTS_CONTEXT_ARGS
   [concl_unifier, normalisers, prems_unifier, retrieval, hint_preprocessor]}
 
 signature TERM_INDEX_UNIFICATION_HINTS_ARGS =
 sig
   structure PA : PARSE_TERM_INDEX_UNIFICATION_HINTS_ARGS
   structure PCA : PARSE_TERM_INDEX_UNIFICATION_HINTS_CONTEXT_ARGS
 
   val PCA_entries_from_PA_entries : ('a, 'b, 'c, 'd, 'e, 'f) PA.entries ->
     ('a, 'b, 'c, 'd, 'e) PCA.entries
   val PA_entries_from_PCA_entries : ('a, 'b, 'c, 'd, 'e) PCA.entries -> 'f ->
     ('a, 'b, 'c, 'd, 'e, 'f) PA.entries
   val UHA_PA_entries_from_PCA_entries : ('a, 'b, 'c, 'd, 'e) PCA.entries ->
     ('a, 'b, 'c) Unification_Hints_Args.PA.entries
 
   structure PM : PARSE_TERM_INDEX_UNIFICATION_HINTS_MODE
   type mode = PM.key
   val parse_mode : mode parser
 
   type hint_prio = Unification_Hints_Base.unif_hint * Prio.prio
   val pretty_hint_prio : Proof.context -> hint_prio -> Pretty.T
 
   val sort_hint_prios : hint_prio list -> hint_prio list
 
   val mk_retrieval : Term_Normalisation.term_normaliser -> ('ti -> term -> hint_prio list) ->
     'ti -> Unification_Hints_Base.hint_retrieval
   val mk_sym_retrieval : Term_Normalisation.term_normaliser -> ('ti -> term -> hint_prio list) ->
     'ti -> Unification_Hints_Base.hint_retrieval
 
   type 'ti args = (Unification_Base.unifier, Unification_Base.normalisers, Unification_Base.unifier,
     'ti -> Unification_Hints_Base.hint_retrieval, Unification_Hints_Base.hint_preprocessor,
     Prio.prio) PA.entries
   type 'ti context_args = (Unification_Base.unifier, Unification_Base.normalisers,
     Unification_Base.unifier, 'ti -> Unification_Hints_Base.hint_retrieval,
     Unification_Hints_Base.hint_preprocessor) PCA.entries
 
   val arg_parsers : (ML_Code_Util.code parser, ML_Code_Util.code parser, ML_Code_Util.code parser,
     ML_Code_Util.code parser, ML_Code_Util.code parser, Prio.prio context_parser) PA.entries
 end
 
 structure Term_Index_Unification_Hints_Args : TERM_INDEX_UNIFICATION_HINTS_ARGS =
 struct
 
 structure UB = Unification_Base
 structure EN = Envir_Normalisation
 structure UHB = Unification_Hints_Base
 structure UHA = Unification_Hints_Args
 structure TUHP = Prio
 
 @{parse_entries (struct) PA
   [concl_unifier, normalisers, prems_unifier, retrieval, hint_preprocessor, prio]}
 
 @{parse_entries (struct) PCA
   [concl_unifier, normalisers, prems_unifier, retrieval, hint_preprocessor]}
 
 fun PCA_entries_from_PA_entries {concl_unifier = concl_unifier, normalisers = normalisers,
   prems_unifier = prems_unifier, retrieval = retrieval, hint_preprocessor = hint_preprocessor,...} =
   {concl_unifier = concl_unifier, normalisers = normalisers, prems_unifier = prems_unifier,
     retrieval = retrieval, hint_preprocessor = hint_preprocessor}
 fun PA_entries_from_PCA_entries {concl_unifier = concl_unifier, normalisers = normalisers,
   prems_unifier = prems_unifier, retrieval = retrieval, hint_preprocessor = hint_preprocessor} prio =
   {concl_unifier = concl_unifier, normalisers = normalisers, prems_unifier = prems_unifier,
     retrieval = retrieval, hint_preprocessor = hint_preprocessor, prio = SOME prio}
 
 fun UHA_PA_entries_from_PCA_entries {concl_unifier = concl_unifier, normalisers = normalisers,
   prems_unifier = prems_unifier,...} =
   {concl_unifier = concl_unifier, normalisers = normalisers, prems_unifier = prems_unifier}
 
 @{parse_entries (struct) PM
   [add, del]}
 type mode = PM.key
 val parse_mode = PM.parse_key
 
 type hint_prio = UHB.unif_hint * TUHP.prio
 
 fun pretty_hint_prio ctxt (hint, prio) = Pretty.block [
     UHB.pretty_hint ctxt hint,
     Pretty.enclose " (" ")" [Pretty.str "priority: ", Prio.pretty prio]
   ]
 
 (*FIXME: use Prio.Table instead of sorted lists*)
 val sort_hint_prios = sort (Prio.ord o apply2 snd)
 
 val hint_seq_of_hint_prios =
   sort_hint_prios
   #> Seq.of_list
   #> Seq.map fst
 
 fun mk_retrieval norm_term retrieve ti _ _ (t, _) _ =
   norm_term t
   |> retrieve ti
   |> hint_seq_of_hint_prios
 
 fun interleave [] ys = ys
   | interleave xs [] = xs
   | interleave (x :: xs) (y :: ys) = x :: y :: interleave xs ys
 
 fun mk_sym_retrieval norm_term retrieve ti _ _ (t1, t2) _ =
   interleave
     (norm_term t1 |> retrieve ti)
     (norm_term t2 |> retrieve ti |> map (apfst Unification_Hints_Base.symmetric_hint))
   |> hint_seq_of_hint_prios
 
 type 'ti args = (UB.unifier, UB.normalisers, UB.unifier, 'ti -> UHB.hint_retrieval,
   UHB.hint_preprocessor, TUHP.prio) PA.entries
 type 'ti context_args = (UB.unifier, UB.normalisers, UB.unifier, 'ti -> UHB.hint_retrieval,
   UHB.hint_preprocessor) PCA.entries
 
 val arg_parsers = {
     concl_unifier = UHA.PA.get_concl_unifier_safe UHA.arg_parsers,
     normalisers = UHA.PA.get_normalisers_safe UHA.arg_parsers,
     prems_unifier = UHA.PA.get_prems_unifier_safe UHA.arg_parsers,
     retrieval = SOME (Parse_Util.nonempty_code (K "retrieval function must not be empty")),
     hint_preprocessor = SOME (Parse_Util.nonempty_code (K "hint preprocessor must not be empty")),
     prio = SOME Prio.parse
   }
 
 end
 
 signature TERM_INDEX_UNIFICATION_HINTS =
 sig
   include HAS_LOGGER
 
   structure UH : UNIFICATION_HINTS
 
   (*underlying term index*)
   structure TI : TERM_INDEX
   structure Data : GENERIC_DATA
 
   val get_retrieval : Context.generic -> Term_Index_Unification_Hints_Args.hint_prio TI.term_index ->
     Unification_Hints_Base.hint_retrieval
   val map_retrieval : (
     (Term_Index_Unification_Hints_Args.hint_prio TI.term_index -> Unification_Hints_Base.hint_retrieval) ->
     Term_Index_Unification_Hints_Args.hint_prio TI.term_index -> Unification_Hints_Base.hint_retrieval) ->
     Context.generic -> Context.generic
 
   val get_hint_preprocessor : Context.generic -> Unification_Hints_Base.hint_preprocessor
   val map_hint_preprocessor : (Unification_Hints_Base.hint_preprocessor ->
     Unification_Hints_Base.hint_preprocessor) -> Context.generic -> Context.generic
 
   val get_index : Context.generic -> Term_Index_Unification_Hints_Args.hint_prio TI.term_index
   val map_index : (Term_Index_Unification_Hints_Args.hint_prio TI.term_index ->
     Term_Index_Unification_Hints_Args.hint_prio TI.term_index) -> Context.generic -> Context.generic
   val pretty_index : Proof.context -> Pretty.T
 
   val add_hint_prio : Term_Index_Unification_Hints_Args.hint_prio -> Context.generic ->
     Context.generic
 
   val del_hint : Unification_Hints_Base.unif_hint -> Context.generic -> Context.generic
 
   val mk_retrieval : Term_Index_Unification_Hints_Args.hint_prio TI.retrieval ->
     Term_Index_Unification_Hints_Args.hint_prio TI.term_index ->
     Unification_Hints_Base.hint_retrieval
   val mk_sym_retrieval : Term_Index_Unification_Hints_Args.hint_prio TI.retrieval ->
     Term_Index_Unification_Hints_Args.hint_prio TI.term_index ->
     Unification_Hints_Base.hint_retrieval
 
   val try_hints : Unification_Base.unifier
 
   val binding : binding
 
   val attribute : (Term_Index_Unification_Hints_Args.mode *
     ((ML_Code_Util.code, ML_Code_Util.code, ML_Code_Util.code,
       ML_Code_Util.code, ML_Code_Util.code, Prio.prio)
       Term_Index_Unification_Hints_Args.PA.entries)) *
     Position.T -> attribute
   val parse_attribute : attribute context_parser
   val setup_attribute : string option -> local_theory -> local_theory
 end
 
 functor Term_Index_Unification_Hints(A : sig
   structure FIA : FUNCTOR_INSTANCE_ARGS
   structure TI : TERM_INDEX
   val init_args : (Term_Index_Unification_Hints_Args.hint_prio TI.term_index)
     Term_Index_Unification_Hints_Args.context_args
   end) : TERM_INDEX_UNIFICATION_HINTS =
 struct
 
 structure UHB = Unification_Hints_Base
 structure TUHA = Term_Index_Unification_Hints_Args
 structure TUHP = Prio
 structure PA = TUHA.PA
 structure PCA = TUHA.PCA
 structure PM = TUHA.PM
 
 structure FIU = Functor_Instance_Util(A.FIA)
 structure TI = A.TI
 
 structure MCU = ML_Code_Util
 structure PU = Parse_Util
 
 val logger = Logger.setup_new_logger Unification_Hints_Base.logger FIU.FIA.full_name
 
 @{functor_instance struct_name = UH
   and functor_name = Unification_Hints
   and accessor = FIU.accessor
   and id = FIU.FIA.id
   and more_args = \<open>val init_args = TUHA.UHA_PA_entries_from_PCA_entries A.init_args\<close>}
 
 fun are_hint_variants ctxt hp =
   let
     val tp = apply2 Thm.prop_of hp
     val env = Unification_Util.empty_envir tp
     fun match tp = First_Order_Unification.match [] ctxt tp env
   in
     match tp
     |> Seq.maps (fn _ => match (swap tp))
     |> not o fst o General_Util.seq_is_empty
   end
 
 (* fun are_hint_prio_variants ctxt ((h1, p1), (h2, p2)) =
   p1 = p2 andalso are_hint_variants ctxt (h1, h2) *)
 
 structure Data = Generic_Data(Pair_Generic_Data_Args(
 struct
   structure Data1 = Pair_Generic_Data_Args(
   struct
     structure Data1 =
     struct
       type T = TUHA.hint_prio TI.term_index -> Unification_Hints_Base.hint_retrieval
       val empty = PCA.get_retrieval A.init_args
       val merge = fst
     end
     structure Data2 =
     struct
       type T = UHB.hint_preprocessor
       val empty = PCA.get_hint_preprocessor A.init_args
       val merge = fst
     end
   end)
   structure Data2 = Term_Index_Generic_Data_Args(
   struct
     type data = TUHA.hint_prio
     structure TI = TI
     fun data_eq ((h1, _), (h2, _))= are_hint_variants (Context.the_local_context ()) (h1, h2)
   end)
 end))
 
 val get_retrieval = fst o fst o Data.get
 val map_retrieval = Data.map o apfst o apfst
 
 val get_hint_preprocessor = snd o fst o Data.get
 val map_hint_preprocessor = Data.map o apfst o apsnd
 
 val get_index = snd o Data.get
 val map_index = Data.map o apsnd
 fun pretty_index ctxt = get_index (Context.Proof ctxt)
   |> TI.content
   |> TUHA.sort_hint_prios
   |> map (TUHA.pretty_hint_prio ctxt)
   |> Pretty.fbreaks
   |> Pretty.block
 
 val term_index_key_from_hint = UHB.cdest_hint_concl #> fst #> Thm.term_of #> TI.norm_term
 
 fun msg_illegal_hint_format ctxt hint = Pretty.block [
     Pretty.str "Illegal hint format for ",
     UHB.pretty_hint ctxt hint
   ] |> Pretty.string_of
 
 fun add_hint_prio (hint, prio) context =
   let
     val ctxt = Context.proof_of context
     val hint = hint |> get_hint_preprocessor context ctxt
     val is_hint_variant = curry (are_hint_variants ctxt) hint o fst
   in
     (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [
         Pretty.str "Adding hint ",
         UHB.pretty_hint ctxt hint
       ] |> Pretty.string_of);
     TI.insert is_hint_variant (term_index_key_from_hint hint, (hint, prio)) (get_index context)
     |> (fn ti => map_index (K ti) context))
     handle Term_Index_Base.INSERT =>
       (@{log Logger.WARN} ctxt
         (fn _ => Pretty.block [
           Pretty.str "Hint ",
           UHB.pretty_hint ctxt hint,
           Pretty.str " already added."
         ] |> Pretty.string_of);
       context)
     | TERM _ => (@{log Logger.WARN} ctxt (fn _ => msg_illegal_hint_format ctxt hint);
       context)
   end
 
 fun del_hint hint context =
   let
     val ctxt = Context.proof_of context
     val hint = hint |> get_hint_preprocessor context ctxt
     val is_hint_variant = curry (are_hint_variants ctxt) hint o fst
   in
     (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [
         Pretty.str "Deleting hint ",
         UHB.pretty_hint ctxt hint
       ] |> Pretty.string_of);
     TI.delete is_hint_variant (term_index_key_from_hint hint) (get_index context)
     |> (fn ti => map_index (K ti) context))
     handle Term_Index_Base.DELETE =>
       (@{log Logger.WARN} ctxt
         (fn _ => Pretty.block [
           Pretty.str "Hint ",
           UHB.pretty_hint ctxt hint,
           Pretty.str " not found."
         ] |> Pretty.string_of);
       context)
     | TERM _ => (@{log Logger.WARN} ctxt (fn _ => msg_illegal_hint_format ctxt hint);
       context)
   end
 
 val mk_retrieval = TUHA.mk_retrieval TI.norm_term
 val mk_sym_retrieval = TUHA.mk_sym_retrieval TI.norm_term
 
 fun try_hints binders ctxt =
   let val context = Context.Proof ctxt
   in UH.try_hints (get_retrieval context (get_index context)) binders ctxt end
 
 val binding = FIU.mk_binding_id_prefix "uhint"
 
 val default_entries = PA.empty_entries () |> fold PA.set_entry [PA.prio TUHP.MEDIUM]
 
 fun parse_arg_entries mode =
   let
     val parsers = TUHA.arg_parsers
     val parse_value = PA.parse_entry (PA.get_concl_unifier parsers |> Scan.lift)
       (PA.get_normalisers parsers |> Scan.lift) (PA.get_prems_unifier parsers |> Scan.lift)
       (PA.get_retrieval parsers |> Scan.lift) (PA.get_hint_preprocessor parsers |> Scan.lift)
       (PA.get_prio parsers)
     val parse_entry = Parse_Key_Value.parse_entry' (Scan.lift PA.parse_key)
       (Scan.lift PU.eq) parse_value
   in
-    PA.parse_entries_required' PU.and_list1' [] parse_entry default_entries
+    PA.parse_entries_required' Parse.and_list1' [] parse_entry default_entries
     |> mode = PM.key PM.del ?
       PU.filter_cut' (is_none o PA.get_prio_safe) (K o K "Priority may not be specified for deletion.")
   end
 
 fun attribute ((mode, entries), pos) =
   let
     fun update_index thm = Term_Util.no_dummy_pattern (Thm.prop_of thm) ? (
       case mode of
         PM.add _ => add_hint_prio (thm, PA.get_prio entries)
       | PM.del _ => del_hint thm)
     val PCA_entries = TUHA.PCA_entries_from_PA_entries entries
     val UHA_PA_entries = TUHA.UHA_PA_entries_from_PCA_entries PCA_entries
     val run_code = ML_Attribute.run_map_context o rpair pos
     fun default_code (context, _) = (SOME context, NONE)
     val map_retrieval = case PCA.get_retrieval_safe PCA_entries of
         SOME c => FIU.code_struct_op "map_retrieval" @ MCU.atomic (MCU.read "K" @ MCU.atomic c)
           |> run_code
       | NONE => default_code
     val map_hint_preprocessor = case PCA.get_hint_preprocessor_safe PCA_entries of
         SOME c => FIU.code_struct_op "map_hint_preprocessor" @ MCU.atomic (MCU.read "K" @ MCU.atomic c)
           |> run_code
       | NONE => default_code
   in
     ML_Attribute_Util.apply_attribute (Thm.declaration_attribute update_index)
     #> ML_Attribute_Util.apply_attribute (UH.attribute (UHA_PA_entries, pos))
     #> ML_Attribute_Util.apply_attribute map_retrieval
     #> map_hint_preprocessor
   end
 
 val parse_attribute =
   (Scan.lift (Scan.optional TUHA.parse_mode (PM.key PM.add))
-  :-- (fn mode => PU.optional' ((Scan.lift Parse.where_ |-- parse_arg_entries mode) |> PU.!!!+)
+  :-- (fn mode => PU.optional' ((Scan.lift Parse.where_ |-- parse_arg_entries mode) |> Parse.!!!!)
     default_entries)
   |> PU.position')
   >> attribute
 
-val setup_attribute = Attrib.local_setup binding (PU.!!!+ parse_attribute) o
+val setup_attribute = Attrib.local_setup binding (Parse.!!!! parse_attribute) o
   the_default ("set unification hints arguments (" ^ FIU.FIA.full_name ^ ")")
 
 end