clarified signature;
authorwenzelm
Mon Jun 03 15:40:08 2019 +0200 (6 weeks ago)
changeset 703087f568724d67e
parent 70307 53d21039518a
child 70309 f9fd15d3cfac
clarified signature;
src/HOL/Decision_Procs/approximation.ML
src/HOL/Library/old_recdef.ML
src/HOL/Real_Asymp/real_asymp_diag.ML
src/HOL/Tools/Function/fun_cases.ML
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
src/HOL/Tools/functor.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/semiring_normalizer.ML
src/HOL/Tools/value_command.ML
src/HOL/ex/Commands.thy
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/specification.ML
src/Pure/Thy/document_antiquotations.ML
src/Pure/Thy/thy_output.ML
src/Pure/simplifier.ML
src/Pure/variable.ML
     1.1 --- a/src/HOL/Decision_Procs/approximation.ML	Mon Jun 03 14:47:27 2019 +0200
     1.2 +++ b/src/HOL/Decision_Procs/approximation.ML	Mon Jun 03 15:40:08 2019 +0200
     1.3 @@ -271,7 +271,7 @@
     1.4      val t = Syntax.read_term ctxt raw_t;
     1.5      val t' = approx 30 ctxt t;
     1.6      val ty' = Term.type_of t';
     1.7 -    val ctxt' = Variable.auto_fixes t' ctxt;
     1.8 +    val ctxt' = Proof_Context.augment t' ctxt;
     1.9    in
    1.10      Print_Mode.with_modes modes (fn () =>
    1.11        Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
     2.1 --- a/src/HOL/Library/old_recdef.ML	Mon Jun 03 14:47:27 2019 +0200
     2.2 +++ b/src/HOL/Library/old_recdef.ML	Mon Jun 03 15:40:08 2019 +0200
     2.3 @@ -1591,7 +1591,7 @@
     2.4  
     2.5  fun prove ctxt strict (t, tac) =
     2.6    let
     2.7 -    val ctxt' = Variable.auto_fixes t ctxt;
     2.8 +    val ctxt' = Proof_Context.augment t ctxt;
     2.9    in
    2.10      if strict
    2.11      then Goal.prove ctxt' [] [] t (K tac)
     3.1 --- a/src/HOL/Real_Asymp/real_asymp_diag.ML	Mon Jun 03 14:47:27 2019 +0200
     3.2 +++ b/src/HOL/Real_Asymp/real_asymp_diag.ML	Mon Jun 03 15:40:08 2019 +0200
     3.3 @@ -122,7 +122,7 @@
     3.4    let
     3.5      val t = prep_term ctxt t
     3.6      val flt = prep_flt ctxt flt
     3.7 -    val ctxt = Variable.auto_fixes t ctxt
     3.8 +    val ctxt = Proof_Context.augment t ctxt
     3.9      val t = reduce_to_at_top flt t
    3.10      val facts = prep_facts ctxt facts
    3.11      val ectxt = mk_eval_ctxt ctxt |> add_facts facts |> set_verbose true
    3.12 @@ -165,7 +165,7 @@
    3.13    let
    3.14      val t = prep_term ctxt t
    3.15      val flt = prep_flt ctxt flt
    3.16 -    val ctxt = Variable.auto_fixes t ctxt
    3.17 +    val ctxt = Proof_Context.augment t ctxt
    3.18      val t = reduce_to_at_top flt t
    3.19      val facts = prep_facts ctxt facts
    3.20      val ectxt = mk_eval_ctxt ctxt |> add_facts facts |> set_verbose true
     4.1 --- a/src/HOL/Tools/Function/fun_cases.ML	Mon Jun 03 14:47:27 2019 +0200
     4.2 +++ b/src/HOL/Tools/Function/fun_cases.ML	Mon Jun 03 15:40:08 2019 +0200
     4.3 @@ -33,7 +33,7 @@
     4.4      fun mk_elim rl =
     4.5        Thm.implies_intr cprop
     4.6          (Tactic.rule_by_tactic ctxt (Inductive.mk_cases_tac ctxt) (Thm.assume cprop RS rl))
     4.7 -      |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
     4.8 +      |> singleton (Variable.export (Proof_Context.augment prop ctxt) ctxt);
     4.9    in
    4.10      (case get_first (try mk_elim) (flat elims) of
    4.11        SOME r => r
     5.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Jun 03 14:47:27 2019 +0200
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Jun 03 15:40:08 2019 +0200
     5.3 @@ -1018,7 +1018,7 @@
     5.4      val t = Syntax.read_term ctxt raw_t
     5.5      val t' = values ctxt soln t
     5.6      val ty' = Term.type_of t'
     5.7 -    val ctxt' = Variable.auto_fixes t' ctxt
     5.8 +    val ctxt' = Proof_Context.augment t' ctxt
     5.9      val _ = tracing "Printing terms..."
    5.10    in
    5.11      Print_Mode.with_modes print_modes (fn () =>
     6.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Jun 03 14:47:27 2019 +0200
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Jun 03 15:40:08 2019 +0200
     6.3 @@ -1648,7 +1648,7 @@
     6.4            binds = [], cases = []}) preds cases_rules
     6.5      val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
     6.6      val lthy'' = lthy'
     6.7 -      |> fold Variable.auto_fixes cases_rules
     6.8 +      |> fold Proof_Context.augment cases_rules
     6.9        |> Proof_Context.update_cases case_env
    6.10      fun after_qed thms goal_ctxt =
    6.11        let
    6.12 @@ -1983,7 +1983,7 @@
    6.13      val t = Syntax.read_term ctxt raw_t
    6.14      val ((t', stats), ctxt') = values param_user_modes options k t ctxt
    6.15      val ty' = Term.type_of t'
    6.16 -    val ctxt'' = Variable.auto_fixes t' ctxt'
    6.17 +    val ctxt'' = Proof_Context.augment t' ctxt'
    6.18      val pretty_stat =
    6.19        (case stats of
    6.20          NONE => []
     7.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Jun 03 14:47:27 2019 +0200
     7.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Jun 03 15:40:08 2019 +0200
     7.3 @@ -318,7 +318,7 @@
     7.4  
     7.5  fun mk_fast_generator_expr ctxt (t, eval_terms) =
     7.6    let
     7.7 -    val ctxt' = Variable.auto_fixes t ctxt
     7.8 +    val ctxt' = Proof_Context.augment t ctxt
     7.9      val names = Term.add_free_names t []
    7.10      val frees = map Free (Term.add_frees t [])
    7.11      fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
    7.12 @@ -351,7 +351,7 @@
    7.13  
    7.14  fun mk_generator_expr ctxt (t, eval_terms) =
    7.15    let
    7.16 -    val ctxt' = Variable.auto_fixes t ctxt
    7.17 +    val ctxt' = Proof_Context.augment t ctxt
    7.18      val names = Term.add_free_names t []
    7.19      val frees = map Free (Term.add_frees t [])
    7.20      fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
    7.21 @@ -374,7 +374,7 @@
    7.22  fun mk_full_generator_expr ctxt (t, eval_terms) =
    7.23    let
    7.24      val thy = Proof_Context.theory_of ctxt
    7.25 -    val ctxt' = Variable.auto_fixes t ctxt
    7.26 +    val ctxt' = Proof_Context.augment t ctxt
    7.27      val names = Term.add_free_names t []
    7.28      val frees = map Free (Term.add_frees t [])
    7.29      val ([depth_name, genuine_only_name], ctxt'') =
    7.30 @@ -415,7 +415,7 @@
    7.31  fun mk_validator_expr ctxt t =
    7.32    let
    7.33      fun bounded_forallT T = (T --> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>natural\<close> --> \<^typ>\<open>bool\<close>
    7.34 -    val ctxt' = Variable.auto_fixes t ctxt
    7.35 +    val ctxt' = Proof_Context.augment t ctxt
    7.36      val names = Term.add_free_names t []
    7.37      val frees = map Free (Term.add_frees t [])
    7.38      fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Jun 03 14:47:27 2019 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Jun 03 15:40:08 2019 +0200
     8.3 @@ -303,7 +303,7 @@
     8.4              |> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
     8.5              |> simplify_spaces
     8.6              |> maybe_quote keywords),
     8.7 -       ctxt |> perhaps (try (Variable.auto_fixes term)))
     8.8 +       ctxt |> perhaps (try (Proof_Context.augment term)))
     8.9  
    8.10      fun using_facts [] [] = ""
    8.11        | using_facts ls ss = enclose "using " " " (space_implode " " (map string_of_label ls @ ss))
    8.12 @@ -323,7 +323,7 @@
    8.13        maybe_quote keywords (simplify_spaces (Print_Mode.setmp [] (Syntax.string_of_typ ctxt) T))
    8.14  
    8.15      fun add_frees xs (s, ctxt) =
    8.16 -      (s ^ space_implode " and " (map of_free xs), ctxt |> fold Variable.auto_fixes (map Free xs))
    8.17 +      (s ^ space_implode " and " (map of_free xs), ctxt |> fold Proof_Context.augment (map Free xs))
    8.18  
    8.19      fun add_fix _ [] = I
    8.20        | add_fix ind xs = add_str (of_indent ind ^ "fix ") #> add_frees xs #> add_str "\n"
     9.1 --- a/src/HOL/Tools/functor.ML	Mon Jun 03 14:47:27 2019 +0200
     9.2 +++ b/src/HOL/Tools/functor.ML	Mon Jun 03 15:40:08 2019 +0200
     9.3 @@ -187,7 +187,7 @@
     9.4        else error ("Illegal additional type variable(s) in term: " ^ Syntax.string_of_term ctxt input_mapper);
     9.5      val _ =
     9.6        if null (Term.add_vars (singleton
     9.7 -        (Variable.export_terms (Variable.auto_fixes input_mapper ctxt) ctxt) input_mapper) [])
     9.8 +        (Variable.export_terms (Proof_Context.augment input_mapper ctxt) ctxt) input_mapper) [])
     9.9        then ()
    9.10        else error ("Illegal locally free variable(s) in term: "
    9.11          ^ Syntax.string_of_term ctxt input_mapper);
    10.1 --- a/src/HOL/Tools/inductive.ML	Mon Jun 03 14:47:27 2019 +0200
    10.2 +++ b/src/HOL/Tools/inductive.ML	Mon Jun 03 15:40:08 2019 +0200
    10.3 @@ -594,7 +594,7 @@
    10.4      fun mk_elim rl =
    10.5        Thm.implies_intr cprop
    10.6          (Tactic.rule_by_tactic ctxt (mk_cases_tac ctxt) (Thm.assume cprop RS rl))
    10.7 -      |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
    10.8 +      |> singleton (Variable.export (Proof_Context.augment prop ctxt) ctxt);
    10.9    in
   10.10      (case get_first (try mk_elim) elims of
   10.11        SOME r => r
   10.12 @@ -642,7 +642,7 @@
   10.13  fun mk_simp_eq ctxt prop =
   10.14    let
   10.15      val thy = Proof_Context.theory_of ctxt;
   10.16 -    val ctxt' = Variable.auto_fixes prop ctxt;
   10.17 +    val ctxt' = Proof_Context.augment prop ctxt;
   10.18      val lhs_of = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of;
   10.19      val substs =
   10.20        retrieve_equations ctxt (HOLogic.dest_Trueprop prop)
    11.1 --- a/src/HOL/Tools/semiring_normalizer.ML	Mon Jun 03 14:47:27 2019 +0200
    11.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Mon Jun 03 15:40:08 2019 +0200
    11.3 @@ -169,7 +169,7 @@
    11.4      {semiring = raw_semiring0, ring = raw_ring0, field = raw_field0, idom = raw_idom, ideal = raw_ideal}
    11.5      lthy =
    11.6    let
    11.7 -    val ctxt' = fold Variable.auto_fixes (fst raw_semiring0 @ fst raw_ring0 @ fst raw_field0) lthy;
    11.8 +    val ctxt' = fold Proof_Context.augment (fst raw_semiring0 @ fst raw_ring0 @ fst raw_field0) lthy;
    11.9      val prepare_ops = apfst (Variable.export_terms ctxt' lthy #> map (Thm.cterm_of lthy));
   11.10      val raw_semiring = prepare_ops raw_semiring0;
   11.11      val raw_ring = prepare_ops raw_ring0;
    12.1 --- a/src/HOL/Tools/value_command.ML	Mon Jun 03 14:47:27 2019 +0200
    12.2 +++ b/src/HOL/Tools/value_command.ML	Mon Jun 03 15:40:08 2019 +0200
    12.3 @@ -55,7 +55,7 @@
    12.4      val t = Syntax.read_term ctxt raw_t;
    12.5      val t' = value_select name ctxt t;
    12.6      val ty' = Term.type_of t';
    12.7 -    val ctxt' = Variable.auto_fixes t' ctxt;
    12.8 +    val ctxt' = Proof_Context.augment t' ctxt;
    12.9      val p = Print_Mode.with_modes modes (fn () =>
   12.10        Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
   12.11          Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
    13.1 --- a/src/HOL/ex/Commands.thy	Mon Jun 03 14:47:27 2019 +0200
    13.2 +++ b/src/HOL/ex/Commands.thy	Mon Jun 03 15:40:08 2019 +0200
    13.3 @@ -20,7 +20,7 @@
    13.4        let
    13.5          val ctxt = Toplevel.context_of st;
    13.6          val t = Syntax.read_term ctxt s;
    13.7 -        val ctxt' = Variable.auto_fixes t ctxt;
    13.8 +        val ctxt' = Proof_Context.augment t ctxt;
    13.9        in Pretty.writeln (Syntax.pretty_term ctxt' t) end)));
   13.10  \<close>
   13.11  
    14.1 --- a/src/Pure/Isar/element.ML	Mon Jun 03 14:47:27 2019 +0200
    14.2 +++ b/src/Pure/Isar/element.ML	Mon Jun 03 15:40:08 2019 +0200
    14.3 @@ -426,7 +426,7 @@
    14.4        let
    14.5          val asms' = Attrib.map_specs (map (Attrib.attribute ctxt)) asms;
    14.6          val (_, ctxt') = ctxt
    14.7 -          |> fold Variable.auto_fixes (maps (map #1 o #2) asms')
    14.8 +          |> fold Proof_Context.augment (maps (map #1 o #2) asms')
    14.9            |> Proof_Context.add_assms Assumption.assume_export asms';
   14.10        in ctxt' end)
   14.11    | init (Defines defs) = Context.map_proof (fn ctxt =>
   14.12 @@ -436,7 +436,7 @@
   14.13              let val (_, t') = Local_Defs.cert_def ctxt (K []) t  (* FIXME adapt ps? *)
   14.14              in (t', (b, [(t', ps)])) end);
   14.15          val (_, ctxt') = ctxt
   14.16 -          |> fold Variable.auto_fixes (map #1 asms)
   14.17 +          |> fold Proof_Context.augment (map #1 asms)
   14.18            |> Proof_Context.add_assms Local_Defs.def_export (map #2 asms);
   14.19        in ctxt' end)
   14.20    | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2
    15.1 --- a/src/Pure/Isar/expression.ML	Mon Jun 03 14:47:27 2019 +0200
    15.2 +++ b/src/Pure/Isar/expression.ML	Mon Jun 03 15:40:08 2019 +0200
    15.3 @@ -184,7 +184,7 @@
    15.4      val (type_parms'', insts'') = chop (length type_parms') checked;
    15.5  
    15.6      (* context *)
    15.7 -    val ctxt' = fold Variable.auto_fixes checked ctxt;
    15.8 +    val ctxt' = fold Proof_Context.augment checked ctxt;
    15.9      val certT = Thm.trim_context_ctyp o Thm.ctyp_of ctxt';
   15.10      val cert = Thm.trim_context_cterm o Thm.cterm_of ctxt';
   15.11  
   15.12 @@ -266,7 +266,7 @@
   15.13    | restore_elem (elem as Lazy_Notes _, _) = elem;
   15.14  
   15.15  fun prep (_, pats) (ctxt, t :: ts) =
   15.16 -  let val ctxt' = Variable.auto_fixes t ctxt
   15.17 +  let val ctxt' = Proof_Context.augment t ctxt
   15.18    in
   15.19      ((t, Syntax.check_props (Proof_Context.set_mode Proof_Context.mode_pattern ctxt') pats),
   15.20        (ctxt', ts))
   15.21 @@ -547,7 +547,7 @@
   15.22  
   15.23      val goal_ctxt = ctxt
   15.24        |> fix_params fixed
   15.25 -      |> (fold o fold) Variable.auto_fixes (propss @ eq_propss);
   15.26 +      |> (fold o fold) Proof_Context.augment (propss @ eq_propss);
   15.27  
   15.28      val export = Variable.export_morphism goal_ctxt ctxt;
   15.29      val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
    16.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Jun 03 14:47:27 2019 +0200
    16.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Jun 03 15:40:08 2019 +0200
    16.3 @@ -255,14 +255,14 @@
    16.4  fun string_of_prop ctxt s =
    16.5    let
    16.6      val prop = Syntax.read_prop ctxt s;
    16.7 -    val ctxt' = Variable.auto_fixes prop ctxt;
    16.8 +    val ctxt' = Proof_Context.augment prop ctxt;
    16.9    in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end;
   16.10  
   16.11  fun string_of_term ctxt s =
   16.12    let
   16.13      val t = Syntax.read_term ctxt s;
   16.14      val T = Term.type_of t;
   16.15 -    val ctxt' = Variable.auto_fixes t ctxt;
   16.16 +    val ctxt' = Proof_Context.augment t ctxt;
   16.17    in
   16.18      Pretty.string_of
   16.19        (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk,
    17.1 --- a/src/Pure/Isar/local_defs.ML	Mon Jun 03 14:47:27 2019 +0200
    17.2 +++ b/src/Pure/Isar/local_defs.ML	Mon Jun 03 15:40:08 2019 +0200
    17.3 @@ -251,7 +251,7 @@
    17.4        |> (abs_def o #2 o cert_def ctxt get_pos);
    17.5      fun prove def_ctxt0 def =
    17.6        let
    17.7 -        val def_ctxt = Variable.auto_fixes prop def_ctxt0;
    17.8 +        val def_ctxt = Proof_Context.augment prop def_ctxt0;
    17.9          val def_thm =
   17.10            Goal.prove def_ctxt [] [] prop
   17.11              (fn {context = goal_ctxt, ...} =>
    18.1 --- a/src/Pure/Isar/proof.ML	Mon Jun 03 14:47:27 2019 +0200
    18.2 +++ b/src/Pure/Isar/proof.ML	Mon Jun 03 15:40:08 2019 +0200
    18.3 @@ -1093,7 +1093,7 @@
    18.4      val (propss, binds) =
    18.5        prep_propp (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) propp;
    18.6      val goal_ctxt = ctxt
    18.7 -      |> (fold o fold) Variable.auto_fixes propss
    18.8 +      |> (fold o fold) Proof_Context.augment propss
    18.9        |> fold Variable.bind_term binds;
   18.10      fun after_qed' (result_ctxt, results) ctxt' = ctxt'
   18.11        |> Proof_Context.restore_naming ctxt
    19.1 --- a/src/Pure/Isar/proof_context.ML	Mon Jun 03 14:47:27 2019 +0200
    19.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Jun 03 15:40:08 2019 +0200
    19.3 @@ -62,6 +62,7 @@
    19.4    val facts_of: Proof.context -> Facts.T
    19.5    val facts_of_fact: Proof.context -> string -> Facts.T
    19.6    val markup_extern_fact: Proof.context -> string -> Markup.T list * xstring
    19.7 +  val augment: term -> Proof.context -> Proof.context
    19.8    val print_name: Proof.context -> string -> string
    19.9    val pretty_name: Proof.context -> string -> Pretty.T
   19.10    val pretty_term_abbrev: Proof.context -> term -> Pretty.T
   19.11 @@ -414,6 +415,14 @@
   19.12    in (markups, xname) end;
   19.13  
   19.14  
   19.15 +(* augment context by implicit term declarations *)
   19.16 +
   19.17 +fun augment t ctxt = ctxt
   19.18 +  |> not (Variable.is_body ctxt) ?
   19.19 +      Variable.add_fixes_direct (rev (Variable.add_free_names ctxt t []))
   19.20 +  |> Variable.declare_term t;
   19.21 +
   19.22 +
   19.23  
   19.24  (** pretty printing **)
   19.25  
    20.1 --- a/src/Pure/Isar/specification.ML	Mon Jun 03 14:47:27 2019 +0200
    20.2 +++ b/src/Pure/Isar/specification.ML	Mon Jun 03 15:40:08 2019 +0200
    20.3 @@ -390,7 +390,7 @@
    20.4    let
    20.5      val (stmt, elems_ctxt) = prep_stmt raw_elems raw_stmt ctxt;
    20.6      val prems = Assumption.local_prems_of elems_ctxt ctxt;
    20.7 -    val stmt_ctxt = fold (fold (Variable.auto_fixes o fst) o snd) stmt elems_ctxt;
    20.8 +    val stmt_ctxt = fold (fold (Proof_Context.augment o fst) o snd) stmt elems_ctxt;
    20.9    in
   20.10      (case raw_stmt of
   20.11        Element.Shows _ =>
    21.1 --- a/src/Pure/Thy/document_antiquotations.ML	Mon Jun 03 14:47:27 2019 +0200
    21.2 +++ b/src/Pure/Thy/document_antiquotations.ML	Mon Jun 03 15:40:08 2019 +0200
    21.3 @@ -43,7 +43,7 @@
    21.4        handle TYPE _ => err ();
    21.5      val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
    21.6      val eq = Logic.mk_equals (t, t');
    21.7 -    val ctxt' = Variable.auto_fixes eq ctxt;
    21.8 +    val ctxt' = Proof_Context.augment eq ctxt;
    21.9    in Proof_Context.pretty_term_abbrev ctxt' eq end;
   21.10  
   21.11  fun pretty_locale ctxt (name, pos) =
    22.1 --- a/src/Pure/Thy/thy_output.ML	Mon Jun 03 14:47:27 2019 +0200
    22.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Jun 03 15:40:08 2019 +0200
    22.3 @@ -466,7 +466,7 @@
    22.4  (* pretty printing *)
    22.5  
    22.6  fun pretty_term ctxt t =
    22.7 -  Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
    22.8 +  Syntax.pretty_term (Proof_Context.augment t ctxt) t;
    22.9  
   22.10  fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
   22.11  
    23.1 --- a/src/Pure/simplifier.ML	Mon Jun 03 14:47:27 2019 +0200
    23.2 +++ b/src/Pure/simplifier.ML	Mon Jun 03 15:40:08 2019 +0200
    23.3 @@ -126,7 +126,7 @@
    23.4  
    23.5  fun make_simproc ctxt name {lhss, proc} =
    23.6    let
    23.7 -    val ctxt' = fold Variable.auto_fixes lhss ctxt;
    23.8 +    val ctxt' = fold Proof_Context.augment lhss ctxt;
    23.9      val lhss' = Variable.export_terms ctxt' ctxt lhss;
   23.10    in
   23.11      cert_simproc (Proof_Context.theory_of ctxt) name {lhss = lhss', proc = proc}
    24.1 --- a/src/Pure/variable.ML	Mon Jun 03 14:47:27 2019 +0200
    24.2 +++ b/src/Pure/variable.ML	Mon Jun 03 15:40:08 2019 +0200
    24.3 @@ -58,7 +58,6 @@
    24.4    val add_fixes_binding: binding list -> Proof.context -> string list * Proof.context
    24.5    val add_fixes: string list -> Proof.context -> string list * Proof.context
    24.6    val add_fixes_direct: string list -> Proof.context -> Proof.context
    24.7 -  val auto_fixes: term -> Proof.context -> Proof.context
    24.8    val fix_dummy_patterns: term -> Proof.context -> term * Proof.context
    24.9    val variant_fixes: string list -> Proof.context -> string list * Proof.context
   24.10    val gen_all: Proof.context -> thm -> thm
   24.11 @@ -476,10 +475,6 @@
   24.12    |> (snd o add_fixes xs)
   24.13    |> restore_body ctxt;
   24.14  
   24.15 -fun auto_fixes t ctxt = ctxt
   24.16 -  |> not (is_body ctxt) ? add_fixes_direct (rev (add_free_names ctxt t []))
   24.17 -  |> declare_term t;
   24.18 -
   24.19  
   24.20  (* dummy patterns *)
   24.21