diff --git a/src/Pure/Isar/expression.ML b/src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML
+++ b/src/Pure/Isar/expression.ML
@@ -1,879 +1,879 @@
 (*  Title:      Pure/Isar/expression.ML
     Author:     Clemens Ballarin, TU Muenchen
 
 Locale expressions and user interface layer of locales.
 *)
 
 signature EXPRESSION =
 sig
   (* Locale expressions *)
   datatype 'term map = Positional of 'term option list | Named of (string * 'term) list
   type 'term rewrites = (Attrib.binding * 'term) list
   type ('name, 'term) expr = ('name * ((string * bool) * ('term map * 'term rewrites))) list
   type expression_i = (string, term) expr * (binding * typ option * mixfix) list
   type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list
 
   (* Processing of context statements *)
   val cert_statement: Element.context_i list -> Element.statement_i ->
     Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context
   val read_statement: Element.context list -> Element.statement ->
     Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context
 
   (* Declaring locales *)
   val cert_declaration: expression_i -> (Proof.context -> Proof.context) ->
     Element.context_i list ->
     Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
       * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
   val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) ->
     Element.context list ->
     Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
       * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
       (*FIXME*)
   val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
     Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
       * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
   val add_locale: binding -> binding -> Bundle.name list ->
     expression_i -> Element.context_i list -> theory -> string * local_theory
   val add_locale_cmd: binding -> binding -> (xstring * Position.T) list ->
     expression -> Element.context list -> theory -> string * local_theory
 
   (* Processing of locale expressions *)
   val cert_goal_expression: expression_i -> Proof.context ->
     (term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context
   val read_goal_expression: expression -> Proof.context ->
     (term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context
 end;
 
 structure Expression : EXPRESSION =
 struct
 
 datatype ctxt = datatype Element.ctxt;
 
 
 (*** Expressions ***)
 
 datatype 'term map =
   Positional of 'term option list |
   Named of (string * 'term) list;
 
 type 'term rewrites = (Attrib.binding * 'term) list;
 
 type ('name, 'term) expr = ('name * ((string * bool) * ('term map * 'term rewrites))) list;
 
 type expression_i = (string, term) expr * (binding * typ option * mixfix) list;
 type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list;
 
 
 (** Internalise locale names in expr **)
 
 fun check_expr thy instances = map (apfst (Locale.check thy)) instances;
 
 
 (** Parameters of expression **)
 
 (*Sanity check of instantiations and extraction of implicit parameters.
   The latter only occurs iff strict = false.
   Positional instantiations are extended to match full length of parameter list
   of instantiated locale.*)
 
 fun parameters_of thy strict (expr, fixed) =
   let
     val ctxt = Proof_Context.init_global thy;
 
     fun reject_dups message xs =
       (case duplicates (op =) xs of
         [] => ()
       | dups => error (message ^ commas dups));
 
     fun parm_eq ((p1, mx1), (p2, mx2)) =
       p1 = p2 andalso
         (Mixfix.equal (mx1, mx2) orelse
           error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression" ^
             Position.here_list [Mixfix.pos_of mx1, Mixfix.pos_of mx2]));
 
     fun params_loc loc = Locale.params_of thy loc |> map (apfst #1);
     fun params_inst (loc, (prfx, (Positional insts, eqns))) =
           let
             val ps = params_loc loc;
             val d = length ps - length insts;
             val insts' =
               if d < 0 then
                 error ("More arguments than parameters in instantiation of locale " ^
                   quote (Locale.markup_name ctxt loc))
               else insts @ replicate d NONE;
             val ps' = (ps ~~ insts') |>
               map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
           in (ps', (loc, (prfx, (Positional insts', eqns)))) end
       | params_inst (loc, (prfx, (Named insts, eqns))) =
           let
             val _ =
               reject_dups "Duplicate instantiation of the following parameter(s): "
                 (map fst insts);
             val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps =>
               if AList.defined (op =) ps p then AList.delete (op =) p ps
               else error (quote p ^ " not a parameter of instantiated expression"));
           in (ps', (loc, (prfx, (Named insts, eqns)))) end;
     fun params_expr is =
       let
         val (is', ps') = fold_map (fn i => fn ps =>
           let
             val (ps', i') = params_inst i;
             val ps'' = distinct parm_eq (ps @ ps');
           in (i', ps'') end) is []
       in (ps', is') end;
 
     val (implicit, expr') = params_expr expr;
 
     val implicit' = map #1 implicit;
     val fixed' = map (Variable.check_name o #1) fixed;
     val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
     val implicit'' =
       if strict then []
       else
         let
           val _ =
             reject_dups
               "Parameter(s) declared simultaneously in expression and for clause: "
               (implicit' @ fixed');
         in map (fn (x, mx) => (Binding.name x, NONE, mx)) implicit end;
 
   in (expr', implicit'' @ fixed) end;
 
 
 (** Read instantiation **)
 
 (* Parse positional or named instantiation *)
 
 local
 
 fun prep_inst prep_term ctxt parms (Positional insts) =
       (insts ~~ parms) |> map
         (fn (NONE, p) => Free (p, dummyT)
           | (SOME t, _) => prep_term ctxt t)
   | prep_inst prep_term ctxt parms (Named insts) =
       parms |> map (fn p =>
         (case AList.lookup (op =) insts p of
           SOME t => prep_term ctxt t |
           NONE => Free (p, dummyT)));
 
 in
 
 fun parse_inst x = prep_inst Syntax.parse_term x;
 fun make_inst x = prep_inst (K I) x;
 
 end;
 
 
 (* Instantiation morphism *)
 
 fun inst_morphism params ((prfx, mandatory), insts') ctxt =
   let
     (* parameters *)
     val parm_types = map #2 params;
     val type_parms = fold Term.add_tfreesT parm_types [];
 
     (* type inference *)
     val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types;
     val type_parms' = fold Term.add_tvarsT parm_types' [];
     val checked =
       (map (Logic.mk_type o TVar) type_parms' @ map2 Type.constraint parm_types' insts')
       |> Syntax.check_terms (Config.put Type_Infer.object_logic false ctxt)
     val (type_parms'', insts'') = chop (length type_parms') checked;
 
     (* context *)
     val ctxt' = fold Proof_Context.augment checked ctxt;
     val certT = Thm.trim_context_ctyp o Thm.ctyp_of ctxt';
     val cert = Thm.trim_context_cterm o Thm.cterm_of ctxt';
 
     (* instantiation *)
     val instT =
       (type_parms ~~ map Logic.dest_type type_parms'')
       |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T));
     val cert_inst =
       ((map #1 params ~~
         map (Term_Subst.instantiateT_frees (TFrees.make instT)) parm_types) ~~ insts'')
       |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t));
   in
     (Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $>
       Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt')
   end;
 
 
 (*** Locale processing ***)
 
 (** Parsing **)
 
 fun parse_elem prep_typ prep_term ctxt =
   Element.map_ctxt
    {binding = I,
     typ = prep_typ ctxt,
     term = prep_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt),
     pattern = prep_term (Proof_Context.set_mode Proof_Context.mode_pattern ctxt),
     fact = I,
     attrib = I};
 
 fun prepare_stmt prep_prop prep_obtains ctxt stmt =
   (case stmt of
     Element.Shows raw_shows =>
       raw_shows |> (map o apsnd o map) (fn (t, ps) =>
         (prep_prop (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) t,
           map (prep_prop (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)) ps))
   | Element.Obtains raw_obtains =>
       let
         val ((_, thesis), thesis_ctxt) = Obtain.obtain_thesis ctxt;
         val obtains = prep_obtains thesis_ctxt thesis raw_obtains;
       in map (fn (b, t) => ((b, []), [(t, [])])) obtains end);
 
 
 (** Simultaneous type inference: instantiations + elements + statement **)
 
 local
 
 fun mk_type T = (Logic.mk_type T, []);
 fun mk_term t = (t, []);
 fun mk_propp (p, pats) = (Type.constraint propT p, pats);
 
 fun dest_type (T, []) = Logic.dest_type T;
 fun dest_term (t, []) = t;
 fun dest_propp (p, pats) = (p, pats);
 
 fun extract_inst (_, (_, ts)) = map mk_term ts;
 fun restore_inst ((l, (p, _)), cs) = (l, (p, map dest_term cs));
 
 fun extract_eqns es = map (mk_term o snd) es;
 fun restore_eqns (es, cs) = map2 (fn (b, _) => fn c => (b, dest_term c)) es cs;
 
 fun extract_elem (Fixes fixes) = map (#2 #> the_list #> map mk_type) fixes
   | extract_elem (Constrains csts) = map (#2 #> single #> map mk_type) csts
   | extract_elem (Assumes asms) = map (#2 #> map mk_propp) asms
   | extract_elem (Defines defs) = map (fn (_, (t, ps)) => [mk_propp (t, ps)]) defs
   | extract_elem (Notes _) = []
   | extract_elem (Lazy_Notes _) = [];
 
 fun restore_elem (Fixes fixes, css) =
       (fixes ~~ css) |> map (fn ((x, _, mx), cs) =>
         (x, cs |> map dest_type |> try hd, mx)) |> Fixes
   | restore_elem (Constrains csts, css) =
       (csts ~~ css) |> map (fn ((x, _), cs) =>
         (x, cs |> map dest_type |> hd)) |> Constrains
   | restore_elem (Assumes asms, css) =
       (asms ~~ css) |> map (fn ((b, _), cs) => (b, map dest_propp cs)) |> Assumes
   | restore_elem (Defines defs, css) =
       (defs ~~ css) |> map (fn ((b, _), [c]) => (b, dest_propp c)) |> Defines
   | restore_elem (elem as Notes _, _) = elem
   | restore_elem (elem as Lazy_Notes _, _) = elem;
 
 fun prep (_, pats) (ctxt, t :: ts) =
   let val ctxt' = Proof_Context.augment t ctxt
   in
     ((t, Syntax.check_props (Proof_Context.set_mode Proof_Context.mode_pattern ctxt') pats),
       (ctxt', ts))
   end;
 
 fun check cs ctxt =
   let
     val (cs', (ctxt', _)) = fold_map prep cs
       (ctxt, Syntax.check_terms
         (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) (map fst cs));
   in (cs', ctxt') end;
 
 in
 
 fun check_autofix insts eqnss elems concl ctxt =
   let
     val inst_cs = map extract_inst insts;
     val eqns_cs = map extract_eqns eqnss;
     val elem_css = map extract_elem elems;
     val concl_cs = (map o map) mk_propp (map snd concl);
     (* Type inference *)
     val (inst_cs' :: eqns_cs' :: css', ctxt') =
       (fold_burrow o fold_burrow) check (inst_cs :: eqns_cs :: elem_css @ [concl_cs]) ctxt;
     val (elem_css', [concl_cs']) = chop (length elem_css) css';
   in
     ((map restore_inst (insts ~~ inst_cs'),
       map restore_eqns (eqnss ~~ eqns_cs'),
       map restore_elem (elems ~~ elem_css'),
       map fst concl ~~ concl_cs'), ctxt')
   end;
 
 end;
 
 
 (** Prepare locale elements **)
 
 fun declare_elem prep_var (Fixes fixes) ctxt =
       let val (vars, _) = fold_map prep_var fixes ctxt
       in ctxt |> Proof_Context.add_fixes vars |> snd end
   | declare_elem prep_var (Constrains csts) ctxt =
       ctxt |> fold_map (fn (x, T) => prep_var (Binding.name x, SOME T, NoSyn)) csts |> snd
   | declare_elem _ (Assumes _) ctxt = ctxt
   | declare_elem _ (Defines _) ctxt = ctxt
   | declare_elem _ (Notes _) ctxt = ctxt
   | declare_elem _ (Lazy_Notes _) ctxt = ctxt;
 
 
 (** Finish locale elements **)
 
 fun finish_inst ctxt (loc, (prfx, inst)) =
   let
     val thy = Proof_Context.theory_of ctxt;
     val (morph, _) = inst_morphism (map #1 (Locale.params_of thy loc)) (prfx, inst) ctxt;
   in (loc, morph) end;
 
 fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) =>
   let val x = Binding.name_of binding
   in (binding, AList.lookup (op =) parms x, mx) end);
 
 local
 
 fun closeup _ _ false elem = elem
   | closeup (outer_ctxt, ctxt) parms true elem =
       let
         (* FIXME consider closing in syntactic phase -- before type checking *)
         fun close_frees t =
           let
             val rev_frees =
               Term.fold_aterms (fn Free (x, T) =>
                 if Variable.is_fixed outer_ctxt x orelse AList.defined (op =) parms x then I
                 else insert (op =) (x, T) | _ => I) t [];
           in fold (Logic.all o Free) rev_frees t end;
 
         fun no_binds [] = []
           | no_binds _ = error "Illegal term bindings in context element";
       in
         (case elem of
           Assumes asms => Assumes (asms |> map (fn (a, propps) =>
             (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
         | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) =>
             let val ((c, _), t') = Local_Defs.cert_def ctxt (K []) (close_frees t)
             in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end))
         | e => e)
       end;
 
 in
 
 fun finish_elem _ parms _ (Fixes fixes) = Fixes (finish_fixes parms fixes)
   | finish_elem _ _ _ (Constrains _) = Constrains []
   | finish_elem ctxts parms do_close (Assumes asms) = closeup ctxts parms do_close (Assumes asms)
   | finish_elem ctxts parms do_close (Defines defs) = closeup ctxts parms do_close (Defines defs)
   | finish_elem _ _ _ (elem as Notes _) = elem
   | finish_elem _ _ _ (elem as Lazy_Notes _) = elem;
 
 end;
 
 
 (** Process full context statement: instantiations + elements + statement **)
 
 (* Interleave incremental parsing and type inference over entire parsed stretch. *)
 
 local
 
 fun abs_def ctxt =
   Thm.cterm_of ctxt #> Assumption.assume ctxt #> Local_Defs.abs_def_rule ctxt #> Thm.prop_of;
 
 fun prep_full_context_statement
     parse_typ parse_prop prep_obtains prep_var_elem prep_inst prep_eqns prep_attr prep_var_inst prep_expr
     {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_stmt ctxt1 =
   let
     val thy = Proof_Context.theory_of ctxt1;
 
     val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
 
     fun prep_insts_cumulative (loc, (prfx, (inst, eqns))) (i, insts, eqnss, ctxt) =
       let
         val params = map #1 (Locale.params_of thy loc);
         val inst' = prep_inst ctxt (map #1 params) inst;
         val parm_types' =
           params |> map (#2 #> Logic.varifyT_global #>
               Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) #>
               Type_Infer.paramify_vars);
         val inst'' = map2 Type.constraint parm_types' inst';
         val insts' = insts @ [(loc, (prfx, inst''))];
         val ((insts'', _, _, _), ctxt2) = check_autofix insts' [] [] [] ctxt;
         val inst''' = insts'' |> List.last |> snd |> snd;
         val (inst_morph, _) = inst_morphism params (prfx, inst''') ctxt;
         val ctxt' = Locale.activate_declarations (loc, inst_morph) ctxt2
           handle ERROR msg => if null eqns then error msg else
             (Locale.tracing ctxt1
              (msg ^ "\nFalling back to reading rewrites clause before activation.");
              ctxt2);
 
         val attrss = map (apsnd (map (prep_attr ctxt)) o fst) eqns;
         val eqns' = (prep_eqns ctxt' o map snd) eqns;
         val eqnss' = [attrss ~~ eqns'];
         val ((_, [eqns''], _, _), _) = check_autofix insts'' eqnss' [] [] ctxt';
         val rewrite_morph = eqns'
           |> map (abs_def ctxt')
           |> Variable.export_terms ctxt' ctxt
           |> Element.eq_term_morphism (Proof_Context.theory_of ctxt)
           |> the_default Morphism.identity;
        val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
        val eqnss' = eqnss @ [attrss ~~ Variable.export_terms ctxt' ctxt eqns'];
       in (i + 1, insts', eqnss', ctxt'') end;
 
     fun prep_elem raw_elem ctxt =
       let
         val ctxt' = ctxt
           |> Context_Position.set_visible false
           |> declare_elem prep_var_elem raw_elem
           |> Context_Position.restore_visible ctxt;
         val elems' = parse_elem parse_typ parse_prop ctxt' raw_elem;
       in (elems', ctxt') end;
 
     val fors = fold_map prep_var_inst fixed ctxt1 |> fst;
     val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd;
     val (_, insts', eqnss', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], [], ctxt2);
 
     fun prep_stmt elems ctxt =
       check_autofix insts' [] elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt;
 
     val _ =
       if fixed_frees then ()
       else
         (case fold (fold (Variable.add_frees ctxt3) o snd o snd) insts' [] of
           [] => ()
         | frees => error ("Illegal free variables in expression: " ^
             commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees))));
 
     val ((insts, _, elems', concl), ctxt4) = ctxt3
       |> init_body
       |> fold_map prep_elem raw_elems
       |-> prep_stmt;
 
 
     (* parameters from expression and elements *)
 
     val xs = maps (fn Fixes fixes => map (Variable.check_name o #1) fixes | _ => [])
       (Fixes fors :: elems');
     val (parms, ctxt5) = fold_map Proof_Context.inferred_param xs ctxt4;
 
     val fors' = finish_fixes parms fors;
     val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors';
     val deps = map (finish_inst ctxt5) insts;
     val elems'' = map (finish_elem (ctxt1, ctxt5) parms do_close) elems';
 
   in ((fixed, deps, eqnss', elems'', concl), (parms, ctxt5)) end;
 
 in
 
 fun cert_full_context_statement x =
   prep_full_context_statement (K I) (K I) Obtain.cert_obtains
     Proof_Context.cert_var make_inst Syntax.check_props (K I) Proof_Context.cert_var (K I) x;
 
 fun cert_read_full_context_statement x =
   prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains
     Proof_Context.read_var make_inst Syntax.check_props (K I) Proof_Context.cert_var (K I) x;
 
 fun read_full_context_statement x =
   prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains
     Proof_Context.read_var parse_inst Syntax.read_props Attrib.check_src Proof_Context.read_var check_expr x;
 
 end;
 
 
 (* Context statement: elements + statement *)
 
 local
 
 fun prep_statement prep activate raw_elems raw_stmt ctxt =
   let
     val ((_, _, _, elems, concl), _) =
       prep {strict = true, do_close = false, fixed_frees = true}
         ([], []) I raw_elems raw_stmt ctxt;
     val ctxt' = ctxt
       |> Proof_Context.set_stmt true
       |> fold_map activate elems |> #2
       |> Proof_Context.restore_stmt ctxt;
   in (concl, ctxt') end;
 
 in
 
 fun cert_statement x = prep_statement cert_full_context_statement Element.activate_i x;
 fun read_statement x = prep_statement read_full_context_statement Element.activate x;
 
 end;
 
 
 (* Locale declaration: import + elements *)
 
 fun fix_params params =
   Proof_Context.add_fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd;
 
 local
 
 fun prep_declaration prep activate raw_import init_body raw_elems ctxt =
   let
     val ((fixed, deps, eqnss, elems, _), (parms, ctxt0)) =
       prep {strict = false, do_close = true, fixed_frees = false}
         raw_import init_body raw_elems (Element.Shows []) ctxt;
     val _ = null (flat eqnss) orelse error "Illegal rewrites clause(s) in declaration of locale";
     (* Declare parameters and imported facts *)
     val ctxt' = ctxt
       |> fix_params fixed
       |> fold (Context.proof_map o Locale.activate_facts NONE) deps;
     val (elems', ctxt'') = ctxt'
       |> Proof_Context.set_stmt true
       |> fold_map activate elems
       ||> Proof_Context.restore_stmt ctxt';
   in ((fixed, deps, elems', ctxt''), (parms, ctxt0)) end;
 
 in
 
 fun cert_declaration x = prep_declaration cert_full_context_statement Element.activate_i x;
 fun cert_read_declaration x = prep_declaration cert_read_full_context_statement Element.activate x;
 fun read_declaration x = prep_declaration read_full_context_statement Element.activate x;
 
 end;
 
 
 (* Locale expression to set up a goal *)
 
 local
 
 fun props_of thy (name, morph) =
   let val (asm, defs) = Locale.specification_of thy name
   in map (Morphism.term morph) (the_list asm @ defs) end;
 
 fun prep_goal_expression prep expression ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
 
     val ((fixed, deps, eqnss, _, _), _) =
       prep {strict = true, do_close = true, fixed_frees = true} expression I []
         (Element.Shows []) ctxt;
     (* proof obligations *)
     val propss = map (props_of thy) deps;
     val eq_propss = (map o map) snd eqnss;
 
     val goal_ctxt = ctxt
       |> fix_params fixed
       |> (fold o fold) Proof_Context.augment (propss @ eq_propss);
 
     val export = Proof_Context.export_morphism goal_ctxt ctxt;
     val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
     val exp_term = Term_Subst.zero_var_indexes o Morphism.term export;
     val exp_typ = Logic.type_map exp_term;
     val export' =
       Morphism.morphism "Expression.prep_goal"
         {binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]};
   in ((propss, eq_propss, deps, eqnss, export'), goal_ctxt) end;
 
 in
 
 fun cert_goal_expression x = prep_goal_expression cert_full_context_statement x;
 fun read_goal_expression x = prep_goal_expression read_full_context_statement x;
 
 end;
 
 
 (*** Locale declarations ***)
 
 (* extract specification text *)
 
 val norm_term = Envir.beta_norm oo Term.subst_atomic;
 
 fun bind_def ctxt eq (env, eqs) =
   let
     val _ = Local_Defs.cert_def ctxt (K []) eq;
     val ((y, T), b) = Local_Defs.abs_def eq;
     val b' = norm_term env b;
     fun err msg = error (msg ^ ": " ^ quote y);
   in
     (case filter (fn (Free (y', _), _) => y = y' | _ => false) env of
       [] => ((Free (y, T), b') :: env, eq :: eqs)
     | dups =>
         if forall (fn (_, b'') => b' aconv b'') dups then (env, eqs)
         else err "Attempt to redefine variable")
   end;
 
 (* text has the following structure:
        (((exts, exts'), (ints, ints')), (xs, env, defs))
    where
      exts: external assumptions (terms in assumes elements)
      exts': dito, normalised wrt. env
      ints: internal assumptions (terms in assumptions from insts)
      ints': dito, normalised wrt. env
      xs: the free variables in exts' and ints' and rhss of definitions,
        this includes parameters except defined parameters
      env: list of term pairs encoding substitutions, where the first term
        is a free variable; substitutions represent defines elements and
        the rhs is normalised wrt. the previous env
      defs: the equations from the defines elements
    *)
 
 fun eval_text _ _ (Fixes _) text = text
   | eval_text _ _ (Constrains _) text = text
   | eval_text _ is_ext (Assumes asms)
         (((exts, exts'), (ints, ints')), (env, defs)) =
       let
         val ts = maps (map #1 o #2) asms;
         val ts' = map (norm_term env) ts;
         val spec' =
           if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
           else ((exts, exts'), (ints @ ts, ints' @ ts'));
       in (spec', (env, defs)) end
   | eval_text ctxt _ (Defines defs) (spec, binds) =
       (spec, fold (bind_def ctxt o #1 o #2) defs binds)
   | eval_text _ _ (Notes _) text = text
   | eval_text _ _ (Lazy_Notes _) text = text;
 
 fun eval_inst ctxt (loc, morph) text =
   let
     val thy = Proof_Context.theory_of ctxt;
     val (asm, defs) = Locale.specification_of thy loc;
     val asm' = Option.map (Morphism.term morph) asm;
     val defs' = map (Morphism.term morph) defs;
     val text' =
       text |>
        (if is_some asm then
           eval_text ctxt false (Assumes [(Binding.empty_atts, [(the asm', [])])])
         else I) |>
        (if not (null defs) then
           eval_text ctxt false (Defines (map (fn def => (Binding.empty_atts, (def, []))) defs'))
         else I)
 (* FIXME clone from locale.ML *)
   in text' end;
 
 fun eval_elem ctxt elem text =
   eval_text ctxt true elem text;
 
 fun eval ctxt deps elems =
   let
     val text' = fold (eval_inst ctxt) deps ((([], []), ([], [])), ([], []));
     val ((spec, (_, defs))) = fold (eval_elem ctxt) elems text';
   in (spec, defs) end;
 
 (* axiomsN: name of theorem set with destruct rules for locale predicates,
      also name suffix of delta predicates and assumptions. *)
 
 val axiomsN = "axioms";
 
 local
 
 (* introN: name of theorems for introduction rules of locale and
      delta predicates *)
 
 val introN = "intro";
 
 fun atomize_spec ctxt ts =
   let
     val t = Logic.mk_conjunction_balanced ts;
     val body = Object_Logic.atomize_term ctxt t;
     val bodyT = Term.fastype_of body;
   in
     if bodyT = propT
     then (t, propT, Thm.reflexive (Thm.cterm_of ctxt t))
     else (body, bodyT, Object_Logic.atomize ctxt (Thm.cterm_of ctxt t))
   end;
 
 (* achieve plain syntax for locale predicates (without "PROP") *)
 
 fun aprop_tr' n c =
   let
     val c' = Lexicon.mark_const c;
     fun tr' (_: Proof.context) T args =
       if T <> dummyT andalso length args = n
       then Syntax.const "_aprop" $ Term.list_comb (Syntax.const c', args)
       else raise Match;
   in (c', tr') end;
 
 (* define one predicate including its intro rule and axioms
    - binding: predicate name
    - parms: locale parameters
    - defs: thms representing substitutions from defines elements
    - ts: terms representing locale assumptions (not normalised wrt. defs)
    - norm_ts: terms representing locale assumptions (normalised wrt. defs)
    - thy: the theory
 *)
 
 fun def_pred binding parms defs ts norm_ts thy =
   let
     val name = Sign.full_name thy binding;
 
     val thy_ctxt = Proof_Context.init_global thy;
 
     val (body, bodyT, body_eq) = atomize_spec thy_ctxt norm_ts;
     val env = Names.build (Names.add_free_names body);
     val xs = filter (Names.defined env o #1) parms;
     val Ts = map #2 xs;
     val type_tfrees = TFrees.build (fold TFrees.add_tfreesT Ts);
     val extra_tfrees =
       TFrees.build (TFrees.add_tfrees_unless (TFrees.defined type_tfrees) body)
-      |> TFrees.list_set |> sort_by #1 |> map TFree;
+      |> TFrees.keys |> map TFree;
     val predT = map Term.itselfT extra_tfrees ---> Ts ---> bodyT;
 
     val args = map Logic.mk_type extra_tfrees @ map Free xs;
     val head = Term.list_comb (Const (name, predT), args);
     val statement = Object_Logic.ensure_propT thy_ctxt head;
 
     val ([pred_def], defs_thy) =
       thy
       |> bodyT = propT ? Sign.typed_print_translation [aprop_tr' (length args) name]
       |> Sign.declare_const_global ((binding, predT), NoSyn) |> snd
       |> Global_Theory.add_defs false [((Thm.def_binding binding, Logic.mk_equals (head, body)), [])];
     val defs_ctxt = Proof_Context.init_global defs_thy |> Variable.declare_term head;
 
     val intro = Goal.prove_global defs_thy [] norm_ts statement
       (fn {context = ctxt, ...} =>
         rewrite_goals_tac ctxt [pred_def] THEN
         compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
         compose_tac defs_ctxt
           (false,
             Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_ctxt) norm_ts), 0) 1);
 
     val conjuncts =
       (Drule.equal_elim_rule2 OF
         [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (Thm.cterm_of defs_ctxt statement))])
       |> Conjunction.elim_balanced (length ts);
 
     val (_, axioms_ctxt) = defs_ctxt
       |> Assumption.add_assumes (maps Thm.chyps_of (defs @ conjuncts));
     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
       Element.prove_witness axioms_ctxt t
        (rewrite_goals_tac axioms_ctxt defs THEN compose_tac axioms_ctxt (false, ax, 0) 1));
   in ((statement, intro, axioms), defs_thy) end;
 
 in
 
 (* main predicate definition function *)
 
 fun define_preds binding parms (((exts, exts'), (ints, ints')), defs) thy =
   let
     val ctxt = Proof_Context.init_global thy;
     val defs' = map (Thm.cterm_of ctxt #> Assumption.assume ctxt #> Drule.abs_def) defs;
 
     val (a_pred, a_intro, a_axioms, thy'') =
       if null exts then (NONE, NONE, [], thy)
       else
         let
           val abinding =
             if null ints then binding else Binding.suffix_name ("_" ^ axiomsN) binding;
           val ((statement, intro, axioms), thy') =
             thy
             |> def_pred abinding parms defs' exts exts';
           val ((_, [intro']), thy'') =
             thy'
             |> Sign.qualified_path true abinding
             |> Global_Theory.note_thms ""
               ((Binding.name introN, []), [([intro], [Locale.unfold_add])])
             ||> Sign.restore_naming thy';
           in (SOME statement, SOME intro', axioms, thy'') end;
     val (b_pred, b_intro, b_axioms, thy'''') =
       if null ints then (NONE, NONE, [], thy'')
       else
         let
           val ((statement, intro, axioms), thy''') =
             thy''
             |> def_pred binding parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
           val ctxt''' = Proof_Context.init_global thy''';
           val ([(_, [intro']), _], thy'''') =
             thy'''
             |> Sign.qualified_path true binding
             |> Global_Theory.note_thmss ""
                  [((Binding.name introN, []), [([intro], [Locale.intro_add])]),
                   ((Binding.name axiomsN, []),
                     [(map (Drule.export_without_context o Element.conclude_witness ctxt''') axioms,
                       [])])]
             ||> Sign.restore_naming thy''';
         in (SOME statement, SOME intro', axioms, thy'''') end;
   in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy'''') end;
 
 end;
 
 
 local
 
 fun assumes_to_notes (Assumes asms) axms =
       fold_map (fn (a, spec) => fn axs =>
           let val (ps, qs) = chop (length spec) axs
           in ((a, [(ps, [])]), qs) end) asms axms
       |> apfst (curry Notes "")
   | assumes_to_notes e axms = (e, axms);
 
 fun defines_to_notes ctxt (Defines defs) =
       Notes ("", map (fn (a, (def, _)) =>
         (a, [([Assumption.assume ctxt (Thm.cterm_of ctxt def)],
           [(Attrib.internal o K) Locale.witness_add])])) defs)
   | defines_to_notes _ e = e;
 
 val is_hyp = fn Assumes _ => true | Defines _ => true | _ => false;
 
 fun gen_add_locale prep_include prep_decl
     binding raw_predicate_binding raw_includes raw_import raw_body thy =
   let
     val name = Sign.full_name thy binding;
     val _ = Locale.defined thy name andalso
       error ("Duplicate definition of locale " ^ quote name);
 
     val ctxt = Proof_Context.init_global thy;
     val includes = map (prep_include ctxt) raw_includes;
 
     val ((fixed, deps, body_elems, _), (parms, ctxt')) =
       ctxt
       |> Bundle.includes includes
       |> prep_decl raw_import I raw_body;
     val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
 
     val type_tfrees = TFrees.build (fold (TFrees.add_tfreesT o #2) parms);
     val extra_tfrees =
       TFrees.build (fold (TFrees.add_tfrees_unless (TFrees.defined type_tfrees)) exts')
-    val extraTs = TFrees.list_set_rev extra_tfrees;
+      |> TFrees.keys;
     val _ =
-      if null extraTs then ()
+      if null extra_tfrees then ()
       else warning ("Additional type variable(s) in locale specification " ^
           Binding.print binding ^ ": " ^
-          commas (map (Syntax.string_of_typ ctxt' o TFree) (sort_by #1 extraTs)));
+          commas (map (Syntax.string_of_typ ctxt' o TFree) extra_tfrees));
 
     val predicate_binding =
       if Binding.is_empty raw_predicate_binding then binding
       else raw_predicate_binding;
     val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
       define_preds predicate_binding parms text thy;
     val pred_ctxt = Proof_Context.init_global thy';
 
     val a_satisfy = Element.satisfy_morphism a_axioms;
     val b_satisfy = Element.satisfy_morphism b_axioms;
 
     val params = fixed @
       maps (fn Fixes fixes =>
         map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fixes | _ => []) body_elems;
     val asm = if is_some b_statement then b_statement else a_statement;
 
     val hyp_spec = filter is_hyp body_elems;
 
     val notes =
       if is_some asm then
         [("", [((Binding.suffix_name ("_" ^ axiomsN) binding, []),
           [([Assumption.assume pred_ctxt (Thm.cterm_of pred_ctxt (the asm))],
             [(Attrib.internal o K) Locale.witness_add])])])]
       else [];
 
     val notes' =
       body_elems
       |> map (defines_to_notes pred_ctxt)
       |> map (Element.transform_ctxt a_satisfy)
       |> (fn elems =>
         fold_map assumes_to_notes elems (map (Element.conclude_witness pred_ctxt) a_axioms))
       |> fst
       |> map (Element.transform_ctxt b_satisfy)
       |> map_filter (fn Notes notes => SOME notes | _ => NONE);
 
     val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps;
     val axioms = map (Element.conclude_witness pred_ctxt) b_axioms;
 
     val loc_ctxt = thy'
-      |> Locale.register_locale binding (extraTs, params)
+      |> Locale.register_locale binding (extra_tfrees, params)
           (asm, rev defs) (a_intro, b_intro) axioms hyp_spec [] (rev notes) (rev deps')
       |> Named_Target.init includes name
       |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
 
   in (name, loc_ctxt) end;
 
 in
 
 val add_locale = gen_add_locale (K I) cert_declaration;
 val add_locale_cmd = gen_add_locale Bundle.check read_declaration;
 
 end;
 
 end;
diff --git a/src/Pure/primitive_defs.ML b/src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML
+++ b/src/Pure/primitive_defs.ML
@@ -1,86 +1,86 @@
 (*  Title:      Pure/primitive_defs.ML
     Author:     Makarius
 
 Primitive definition forms.
 *)
 
 signature PRIMITIVE_DEFS =
 sig
   val dest_def: Proof.context ->
     {check_head: term -> bool,
      check_free_lhs: string -> bool,
      check_free_rhs: string -> bool,
      check_tfree: string -> bool} ->
     term -> (term * term) * term list * term
   val abs_def: term -> term * term
 end;
 
 structure Primitive_Defs: PRIMITIVE_DEFS =
 struct
 
 fun term_kind (Const _) = "existing constant "
   | term_kind (Free _) = "free variable "
   | term_kind (Bound _) = "bound variable "
   | term_kind _ = "";
 
 (*c x \<equiv> t[x] to \<And>x. c x \<equiv> t[x]*)
 fun dest_def ctxt {check_head, check_free_lhs, check_free_rhs, check_tfree} eq =
   let
     fun err msg = raise TERM (msg, [eq]);
     val eq_vars = Term.strip_all_vars eq;
     val eq_body = Term.strip_all_body eq;
 
     val display_terms =
       commas_quote o map (Syntax.string_of_term ctxt o Syntax_Trans.bound_vars eq_vars);
     val display_types = commas_quote o map (Syntax.string_of_typ ctxt);
 
     val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (\<equiv>)";
     val lhs = Envir.beta_eta_contract raw_lhs;
     val (head, args) = Term.strip_comb lhs;
     val head_tfrees = TFrees.build (TFrees.add_tfrees head);
 
     fun check_arg (Bound _) = true
       | check_arg (Free (x, _)) = check_free_lhs x
       | check_arg (Const ("Pure.type", Type ("itself", [TFree _]))) = true
       | check_arg _ = false;
     fun close_arg (Bound _) t = t
       | close_arg x t = Logic.all x t;
 
     val lhs_bads = filter_out check_arg args;
     val lhs_dups = duplicates (op aconv) args;
     val rhs_extras = Term.fold_aterms (fn v as Free (x, _) =>
       if check_free_rhs x orelse member (op aconv) args v then I
       else insert (op aconv) v | _ => I) rhs [];
     val rhs_extrasT =
       TFrees.build (rhs |> TFrees.add_tfrees_unless
         (fn (a, S) => check_tfree a orelse TFrees.defined head_tfrees (a, S)))
-      |> TFrees.list_set_rev |> map TFree;
+      |> TFrees.keys |> map TFree;
   in
     if not (check_head head) then
       err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head])
     else if not (null lhs_bads) then
       err ("Bad arguments on lhs: " ^ display_terms lhs_bads)
     else if not (null lhs_dups) then
       err ("Duplicate arguments on lhs: " ^ display_terms lhs_dups)
     else if not (null rhs_extras) then
       err ("Extra variables on rhs: " ^ display_terms rhs_extras)
     else if not (null rhs_extrasT) then
       err ("Extra type variables on rhs: " ^ display_types rhs_extrasT)
     else if exists_subterm (fn t => t aconv head) rhs then
       err "Entity to be defined occurs on rhs"
     else
       ((lhs, rhs), args,
         fold_rev close_arg args (Logic.list_all (eq_vars, (Logic.mk_equals (lhs, rhs)))))
   end;
 
 (*\<And>x. c x \<equiv> t[x] to c \<equiv> \<lambda>x. t[x]*)
 fun abs_def eq =
   let
     val body = Term.strip_all_body eq;
     val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
     val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body));
     val (lhs', args) = Term.strip_comb lhs;
     val rhs' = fold_rev (absfree o dest_Free) args rhs;
   in (lhs', rhs') end;
 
 end;
diff --git a/src/Pure/theory.ML b/src/Pure/theory.ML
--- a/src/Pure/theory.ML
+++ b/src/Pure/theory.ML
@@ -1,342 +1,342 @@
 (*  Title:      Pure/theory.ML
     Author:     Lawrence C Paulson and Markus Wenzel
 
 Logical theory content: axioms, definitions, and begin/end wrappers.
 *)
 
 signature THEORY =
 sig
   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
   val nodes_of: theory -> theory list
   val setup: (theory -> theory) -> unit
   val local_setup: (Proof.context -> Proof.context) -> unit
   val install_pure: theory -> unit
   val get_pure: unit -> theory
   val get_pure_bootstrap: unit -> theory
   val get_markup: theory -> Markup.T
   val check: {long: bool} -> Proof.context -> string * Position.T -> theory
   val axiom_table: theory -> term Name_Space.table
   val axiom_space: theory -> Name_Space.T
   val all_axioms_of: theory -> (string * term) list
   val defs_of: theory -> Defs.T
   val at_begin: (theory -> theory option) -> theory -> theory
   val at_end: (theory -> theory option) -> theory -> theory
   val join_theory: theory list -> theory
   val begin_theory: string * Position.T -> theory list -> theory
   val end_theory: theory -> theory
   val add_axiom: Proof.context -> binding * term -> theory -> theory
   val const_dep: theory -> string * typ -> Defs.entry
   val type_dep: string * typ list -> Defs.entry
   val add_deps: Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory
   val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory
   val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory
   val specify_const: (binding * typ) * mixfix -> theory -> term * theory
   val check_overloading: Proof.context -> bool -> string * typ -> unit
 end
 
 structure Theory: THEORY =
 struct
 
 
 (** theory context operations **)
 
 val parents_of = Context.parents_of;
 val ancestors_of = Context.ancestors_of;
 fun nodes_of thy = thy :: ancestors_of thy;
 
 fun setup f = Context.>> (Context.map_theory f);
 fun local_setup f = Context.>> (Context.map_proof f);
 
 
 (* implicit theory Pure *)
 
 val pure: theory Single_Assignment.var = Single_Assignment.var "pure";
 
 fun install_pure thy = Single_Assignment.assign pure thy;
 
 fun get_pure () =
   (case Single_Assignment.peek pure of
     SOME thy => thy
   | NONE => raise Fail "Theory Pure not present");
 
 fun get_pure_bootstrap () =
   (case Single_Assignment.peek pure of
     SOME thy => thy
   | NONE => Context.the_global_context ());
 
 
 
 (** datatype thy **)
 
 type wrapper = (theory -> theory option) * stamp;
 
 fun apply_wrappers (wrappers: wrapper list) =
   perhaps (perhaps_loop (perhaps_apply (map fst wrappers)));
 
 datatype thy = Thy of
  {pos: Position.T,
   id: serial,
   axioms: term Name_Space.table,
   defs: Defs.T,
   wrappers: wrapper list * wrapper list};
 
 fun make_thy (pos, id, axioms, defs, wrappers) =
   Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers};
 
 structure Thy = Theory_Data'
 (
   type T = thy;
   val extend = I;
   val empty = make_thy (Position.none, 0, Name_Space.empty_table Markup.axiomN, Defs.empty, ([], []));
   fun merge old_thys (thy1, thy2) =
     let
       val Thy {pos, id, axioms = axioms1, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
       val Thy {pos = _, id = _, axioms = axioms2, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
 
       val axioms' = Name_Space.merge_tables (axioms1, axioms2);
       val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2);
       val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
       val ens' = Library.merge (eq_snd op =) (ens1, ens2);
     in make_thy (pos, id, axioms', defs', (bgs', ens')) end;
 );
 
 fun rep_theory thy = Thy.get thy |> (fn Thy args => args);
 
 fun map_thy f = Thy.map (fn (Thy {pos, id, axioms, defs, wrappers}) =>
   make_thy (f (pos, id, axioms, defs, wrappers)));
 
 fun map_axioms f =
   map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, f axioms, defs, wrappers));
 
 fun map_defs f =
   map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, f defs, wrappers));
 
 fun map_wrappers f =
   map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, defs, f wrappers));
 
 
 (* entity markup *)
 
 fun theory_markup def name id pos =
   if id = 0 then Markup.empty
   else Position.make_entity_markup def id Markup.theoryN (name, pos);
 
 fun init_markup (name, pos) thy =
   let
     val id = serial ();
     val _ = Context_Position.reports_global thy [(pos, theory_markup {def = true} name id pos)];
   in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end;
 
 fun get_markup thy =
   let val {pos, id, ...} = rep_theory thy
   in theory_markup {def = false} (Context.theory_long_name thy) id pos end;
 
 fun check long ctxt (name, pos) =
   let
     val thy = Proof_Context.theory_of ctxt;
     val thy' =
       Context.get_theory long thy name
         handle ERROR msg =>
           let
             val completion_report =
               Completion.make_report (name, pos)
                 (fn completed =>
                   map (Context.theory_name' long) (ancestors_of thy)
                   |> filter (completed o Long_Name.base_name)
                   |> sort_strings
                   |> map (fn a => (a, (Markup.theoryN, a))));
           in error (msg ^ Position.here pos ^ completion_report) end;
     val _ = Context_Position.report ctxt pos (get_markup thy');
   in thy' end;
 
 
 (* basic operations *)
 
 val axiom_table = #axioms o rep_theory;
 val axiom_space = Name_Space.space_of_table o axiom_table;
 
 val all_axioms_of = Name_Space.dest_table o axiom_table;
 
 val defs_of = #defs o rep_theory;
 
 
 (* join theory *)
 
 fun join_theory [] = raise List.Empty
   | join_theory [thy] = thy
   | join_theory thys = foldl1 Context.join_thys thys;
 
 
 (* begin/end theory *)
 
 val begin_wrappers = rev o #1 o #wrappers o rep_theory;
 val end_wrappers = rev o #2 o #wrappers o rep_theory;
 
 fun at_begin f = map_wrappers (apfst (cons (f, stamp ())));
 fun at_end f = map_wrappers (apsnd (cons (f, stamp ())));
 
 fun begin_theory (name, pos) imports =
   if name = Context.PureN then
     (case imports of
       [thy] => init_markup (name, pos) thy
     | _ => error "Bad bootstrapping of theory Pure")
   else
     let
       val thy = Context.begin_thy name imports;
       val wrappers = begin_wrappers thy;
     in
       thy
       |> init_markup (name, pos)
       |> Sign.init_naming
       |> Sign.local_path
       |> apply_wrappers wrappers
       |> tap (Syntax.force_syntax o Sign.syn_of)
     end;
 
 fun end_theory thy =
   thy
   |> apply_wrappers (end_wrappers thy)
   |> Sign.change_check
   |> Context.finish_thy;
 
 
 
 (** primitive specifications **)
 
 (* raw axioms *)
 
 fun cert_axm ctxt (b, raw_tm) =
   let
     val thy = Proof_Context.theory_of ctxt;
     val t = Sign.cert_prop thy raw_tm
       handle TYPE (msg, _, _) => error msg
         | TERM (msg, _) => error msg;
     val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
 
     val bad_sorts =
       rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []);
     val _ = null bad_sorts orelse
       error ("Illegal sort constraints in primitive specification: " ^
         commas (map (Syntax.string_of_typ (Config.put show_sorts true ctxt)) bad_sorts));
   in (b, Sign.no_vars ctxt t) end
   handle ERROR msg => cat_error msg ("The error(s) above occurred in axiom " ^ Binding.print b);
 
 fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms =>
   let
     val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm);
     val context = ctxt
       |> Sign.inherit_naming thy
       |> Context_Position.set_visible_generic false;
     val (_, axioms') = Name_Space.define context true axm axioms;
   in axioms' end);
 
 
 (* dependencies *)
 
 fun const_dep thy (c, T) = ((Defs.Const, c), Sign.const_typargs thy (c, T));
 fun type_dep (c, args) = ((Defs.Type, c), args);
 
 fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs =
   let
     fun prep (item, args) =
       (case fold Term.add_tvarsT args [] of
         [] => (item, map Logic.varifyT_global args)
       | vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, []));
 
     val lhs_vars = TFrees.build (fold TFrees.add_tfreesT (snd lhs));
     val rhs_extras =
       TFrees.build (rhs |> fold (fold (TFrees.add_tfreesT_unless (TFrees.defined lhs_vars)) o snd))
-      |> TFrees.list_set_rev;
+      |> TFrees.keys;
     val _ =
       if null rhs_extras then ()
       else error ("Specification depends on extra type variables: " ^
         commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
         "\nThe error(s) above occurred in " ^ quote description);
   in Defs.define context unchecked def description (prep lhs) (map prep rhs) end;
 
 fun cert_entry thy ((Defs.Const, c), args) =
       Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args)))
       |> dest_Const |> const_dep thy
   | cert_entry thy ((Defs.Type, c), args) =
       Sign.certify_typ thy (Type (c, args)) |> dest_Type |> type_dep;
 
 fun add_deps context a raw_lhs raw_rhs thy =
   let
     val (lhs as ((_, lhs_name), _)) :: rhs = map (cert_entry thy) (raw_lhs :: raw_rhs);
     val description = if a = "" then lhs_name ^ " axiom" else a;
   in thy |> map_defs (dependencies context false NONE description lhs rhs) end;
 
 fun add_deps_global a x y thy =
   add_deps (Defs.global_context thy) a x y thy;
 
 fun specify_const decl thy =
   let val (t, thy') = Sign.declare_const_global decl thy;
   in (t, add_deps_global "" (const_dep thy' (dest_Const t)) [] thy') end;
 
 
 (* overloading *)
 
 fun check_overloading ctxt overloaded (c, T) =
   let
     val thy = Proof_Context.theory_of ctxt;
 
     val declT = Sign.the_const_constraint thy c
       handle TYPE (msg, _, _) => error msg;
     val T' = Logic.varifyT_global T;
 
     fun message sorts txt =
       [Pretty.block [Pretty.str "Specification of constant ",
         Pretty.str c, Pretty.str " ::", Pretty.brk 1,
         Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)],
         Pretty.str txt] |> Pretty.chunks |> Pretty.string_of;
   in
     if Sign.typ_instance thy (declT, T') then ()
     else if Type.raw_instance (declT, T') then
       error (message true "imposes additional sort constraints on the constant declaration")
     else if overloaded then ()
     else
       error (message false "is strictly less general than the declared type (overloading required)")
   end;
 
 
 (* definitional axioms *)
 
 local
 
 fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs =
   let
     val name = Sign.full_name thy b;
     val ((lhs, rhs), _, _) =
       Primitive_Defs.dest_def ctxt
         {check_head = Term.is_Const,
          check_free_lhs = K true,
          check_free_rhs = K false,
          check_tfree = K false} tm
       handle TERM (msg, _) => error msg;
     val lhs_const = Term.dest_Const (Term.head_of lhs);
 
     val rhs_consts =
       fold_aterms (fn Const const => insert (op =) (const_dep thy const) | _ => I) rhs [];
     val rhs_types =
       (fold_types o fold_subtypes) (fn Type t => insert (op =) (type_dep t) | _ => I) rhs [];
     val rhs_deps = rhs_consts @ rhs_types;
 
     val _ = check_overloading ctxt overloaded lhs_const;
   in defs |> dependencies context unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end
   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
    [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"),
     Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)]));
 
 in
 
 fun add_def (context as (ctxt, _)) unchecked overloaded raw_axm thy =
   let val axm = cert_axm ctxt raw_axm in
     thy
     |> map_defs (check_def context thy unchecked overloaded axm)
     |> add_axiom ctxt axm
   end;
 
 end;
 
 end;