--- a/src/HOL/Decision_Procs/approximation.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/HOL/Decision_Procs/approximation.ML Mon Jun 03 15:40:08 2019 +0200
@@ -271,7 +271,7 @@
val t = Syntax.read_term ctxt raw_t;
val t' = approx 30 ctxt t;
val ty' = Term.type_of t';
- val ctxt' = Variable.auto_fixes t' ctxt;
+ val ctxt' = Proof_Context.augment t' ctxt;
in
Print_Mode.with_modes modes (fn () =>
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
--- a/src/HOL/Library/old_recdef.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/HOL/Library/old_recdef.ML Mon Jun 03 15:40:08 2019 +0200
@@ -1591,7 +1591,7 @@
fun prove ctxt strict (t, tac) =
let
- val ctxt' = Variable.auto_fixes t ctxt;
+ val ctxt' = Proof_Context.augment t ctxt;
in
if strict
then Goal.prove ctxt' [] [] t (K tac)
--- a/src/HOL/Real_Asymp/real_asymp_diag.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/HOL/Real_Asymp/real_asymp_diag.ML Mon Jun 03 15:40:08 2019 +0200
@@ -122,7 +122,7 @@
let
val t = prep_term ctxt t
val flt = prep_flt ctxt flt
- val ctxt = Variable.auto_fixes t ctxt
+ val ctxt = Proof_Context.augment t ctxt
val t = reduce_to_at_top flt t
val facts = prep_facts ctxt facts
val ectxt = mk_eval_ctxt ctxt |> add_facts facts |> set_verbose true
@@ -165,7 +165,7 @@
let
val t = prep_term ctxt t
val flt = prep_flt ctxt flt
- val ctxt = Variable.auto_fixes t ctxt
+ val ctxt = Proof_Context.augment t ctxt
val t = reduce_to_at_top flt t
val facts = prep_facts ctxt facts
val ectxt = mk_eval_ctxt ctxt |> add_facts facts |> set_verbose true
--- a/src/HOL/Tools/Function/fun_cases.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/HOL/Tools/Function/fun_cases.ML Mon Jun 03 15:40:08 2019 +0200
@@ -33,7 +33,7 @@
fun mk_elim rl =
Thm.implies_intr cprop
(Tactic.rule_by_tactic ctxt (Inductive.mk_cases_tac ctxt) (Thm.assume cprop RS rl))
- |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
+ |> singleton (Variable.export (Proof_Context.augment prop ctxt) ctxt);
in
(case get_first (try mk_elim) (flat elims) of
SOME r => r
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Jun 03 15:40:08 2019 +0200
@@ -1018,7 +1018,7 @@
val t = Syntax.read_term ctxt raw_t
val t' = values ctxt soln t
val ty' = Term.type_of t'
- val ctxt' = Variable.auto_fixes t' ctxt
+ val ctxt' = Proof_Context.augment t' ctxt
val _ = tracing "Printing terms..."
in
Print_Mode.with_modes print_modes (fn () =>
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Jun 03 15:40:08 2019 +0200
@@ -1648,7 +1648,7 @@
binds = [], cases = []}) preds cases_rules
val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
val lthy'' = lthy'
- |> fold Variable.auto_fixes cases_rules
+ |> fold Proof_Context.augment cases_rules
|> Proof_Context.update_cases case_env
fun after_qed thms goal_ctxt =
let
@@ -1983,7 +1983,7 @@
val t = Syntax.read_term ctxt raw_t
val ((t', stats), ctxt') = values param_user_modes options k t ctxt
val ty' = Term.type_of t'
- val ctxt'' = Variable.auto_fixes t' ctxt'
+ val ctxt'' = Proof_Context.augment t' ctxt'
val pretty_stat =
(case stats of
NONE => []
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Jun 03 15:40:08 2019 +0200
@@ -318,7 +318,7 @@
fun mk_fast_generator_expr ctxt (t, eval_terms) =
let
- val ctxt' = Variable.auto_fixes t ctxt
+ val ctxt' = Proof_Context.augment t ctxt
val names = Term.add_free_names t []
val frees = map Free (Term.add_frees t [])
fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
@@ -351,7 +351,7 @@
fun mk_generator_expr ctxt (t, eval_terms) =
let
- val ctxt' = Variable.auto_fixes t ctxt
+ val ctxt' = Proof_Context.augment t ctxt
val names = Term.add_free_names t []
val frees = map Free (Term.add_frees t [])
fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
@@ -374,7 +374,7 @@
fun mk_full_generator_expr ctxt (t, eval_terms) =
let
val thy = Proof_Context.theory_of ctxt
- val ctxt' = Variable.auto_fixes t ctxt
+ val ctxt' = Proof_Context.augment t ctxt
val names = Term.add_free_names t []
val frees = map Free (Term.add_frees t [])
val ([depth_name, genuine_only_name], ctxt'') =
@@ -415,7 +415,7 @@
fun mk_validator_expr ctxt t =
let
fun bounded_forallT T = (T --> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>natural\<close> --> \<^typ>\<open>bool\<close>
- val ctxt' = Variable.auto_fixes t ctxt
+ val ctxt' = Proof_Context.augment t ctxt
val names = Term.add_free_names t []
val frees = map Free (Term.add_frees t [])
fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Jun 03 15:40:08 2019 +0200
@@ -303,7 +303,7 @@
|> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
|> simplify_spaces
|> maybe_quote keywords),
- ctxt |> perhaps (try (Variable.auto_fixes term)))
+ ctxt |> perhaps (try (Proof_Context.augment term)))
fun using_facts [] [] = ""
| using_facts ls ss = enclose "using " " " (space_implode " " (map string_of_label ls @ ss))
@@ -323,7 +323,7 @@
maybe_quote keywords (simplify_spaces (Print_Mode.setmp [] (Syntax.string_of_typ ctxt) T))
fun add_frees xs (s, ctxt) =
- (s ^ space_implode " and " (map of_free xs), ctxt |> fold Variable.auto_fixes (map Free xs))
+ (s ^ space_implode " and " (map of_free xs), ctxt |> fold Proof_Context.augment (map Free xs))
fun add_fix _ [] = I
| add_fix ind xs = add_str (of_indent ind ^ "fix ") #> add_frees xs #> add_str "\n"
--- a/src/HOL/Tools/functor.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/HOL/Tools/functor.ML Mon Jun 03 15:40:08 2019 +0200
@@ -187,7 +187,7 @@
else error ("Illegal additional type variable(s) in term: " ^ Syntax.string_of_term ctxt input_mapper);
val _ =
if null (Term.add_vars (singleton
- (Variable.export_terms (Variable.auto_fixes input_mapper ctxt) ctxt) input_mapper) [])
+ (Variable.export_terms (Proof_Context.augment input_mapper ctxt) ctxt) input_mapper) [])
then ()
else error ("Illegal locally free variable(s) in term: "
^ Syntax.string_of_term ctxt input_mapper);
--- a/src/HOL/Tools/inductive.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/HOL/Tools/inductive.ML Mon Jun 03 15:40:08 2019 +0200
@@ -594,7 +594,7 @@
fun mk_elim rl =
Thm.implies_intr cprop
(Tactic.rule_by_tactic ctxt (mk_cases_tac ctxt) (Thm.assume cprop RS rl))
- |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
+ |> singleton (Variable.export (Proof_Context.augment prop ctxt) ctxt);
in
(case get_first (try mk_elim) elims of
SOME r => r
@@ -642,7 +642,7 @@
fun mk_simp_eq ctxt prop =
let
val thy = Proof_Context.theory_of ctxt;
- val ctxt' = Variable.auto_fixes prop ctxt;
+ val ctxt' = Proof_Context.augment prop ctxt;
val lhs_of = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of;
val substs =
retrieve_equations ctxt (HOLogic.dest_Trueprop prop)
--- a/src/HOL/Tools/semiring_normalizer.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML Mon Jun 03 15:40:08 2019 +0200
@@ -169,7 +169,7 @@
{semiring = raw_semiring0, ring = raw_ring0, field = raw_field0, idom = raw_idom, ideal = raw_ideal}
lthy =
let
- val ctxt' = fold Variable.auto_fixes (fst raw_semiring0 @ fst raw_ring0 @ fst raw_field0) lthy;
+ val ctxt' = fold Proof_Context.augment (fst raw_semiring0 @ fst raw_ring0 @ fst raw_field0) lthy;
val prepare_ops = apfst (Variable.export_terms ctxt' lthy #> map (Thm.cterm_of lthy));
val raw_semiring = prepare_ops raw_semiring0;
val raw_ring = prepare_ops raw_ring0;
--- a/src/HOL/Tools/value_command.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/HOL/Tools/value_command.ML Mon Jun 03 15:40:08 2019 +0200
@@ -55,7 +55,7 @@
val t = Syntax.read_term ctxt raw_t;
val t' = value_select name ctxt t;
val ty' = Term.type_of t';
- val ctxt' = Variable.auto_fixes t' ctxt;
+ val ctxt' = Proof_Context.augment t' ctxt;
val p = Print_Mode.with_modes modes (fn () =>
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
--- a/src/HOL/ex/Commands.thy Mon Jun 03 14:47:27 2019 +0200
+++ b/src/HOL/ex/Commands.thy Mon Jun 03 15:40:08 2019 +0200
@@ -20,7 +20,7 @@
let
val ctxt = Toplevel.context_of st;
val t = Syntax.read_term ctxt s;
- val ctxt' = Variable.auto_fixes t ctxt;
+ val ctxt' = Proof_Context.augment t ctxt;
in Pretty.writeln (Syntax.pretty_term ctxt' t) end)));
\<close>
--- a/src/Pure/Isar/element.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/Pure/Isar/element.ML Mon Jun 03 15:40:08 2019 +0200
@@ -426,7 +426,7 @@
let
val asms' = Attrib.map_specs (map (Attrib.attribute ctxt)) asms;
val (_, ctxt') = ctxt
- |> fold Variable.auto_fixes (maps (map #1 o #2) asms')
+ |> fold Proof_Context.augment (maps (map #1 o #2) asms')
|> Proof_Context.add_assms Assumption.assume_export asms';
in ctxt' end)
| init (Defines defs) = Context.map_proof (fn ctxt =>
@@ -436,7 +436,7 @@
let val (_, t') = Local_Defs.cert_def ctxt (K []) t (* FIXME adapt ps? *)
in (t', (b, [(t', ps)])) end);
val (_, ctxt') = ctxt
- |> fold Variable.auto_fixes (map #1 asms)
+ |> fold Proof_Context.augment (map #1 asms)
|> Proof_Context.add_assms Local_Defs.def_export (map #2 asms);
in ctxt' end)
| init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2
--- a/src/Pure/Isar/expression.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/Pure/Isar/expression.ML Mon Jun 03 15:40:08 2019 +0200
@@ -184,7 +184,7 @@
val (type_parms'', insts'') = chop (length type_parms') checked;
(* context *)
- val ctxt' = fold Variable.auto_fixes checked ctxt;
+ 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';
@@ -266,7 +266,7 @@
| restore_elem (elem as Lazy_Notes _, _) = elem;
fun prep (_, pats) (ctxt, t :: ts) =
- let val ctxt' = Variable.auto_fixes t ctxt
+ 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))
@@ -547,7 +547,7 @@
val goal_ctxt = ctxt
|> fix_params fixed
- |> (fold o fold) Variable.auto_fixes (propss @ eq_propss);
+ |> (fold o fold) Proof_Context.augment (propss @ eq_propss);
val export = Variable.export_morphism goal_ctxt ctxt;
val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
--- a/src/Pure/Isar/isar_cmd.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Mon Jun 03 15:40:08 2019 +0200
@@ -255,14 +255,14 @@
fun string_of_prop ctxt s =
let
val prop = Syntax.read_prop ctxt s;
- val ctxt' = Variable.auto_fixes prop ctxt;
+ val ctxt' = Proof_Context.augment prop ctxt;
in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end;
fun string_of_term ctxt s =
let
val t = Syntax.read_term ctxt s;
val T = Term.type_of t;
- val ctxt' = Variable.auto_fixes t ctxt;
+ val ctxt' = Proof_Context.augment t ctxt;
in
Pretty.string_of
(Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk,
--- a/src/Pure/Isar/local_defs.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/Pure/Isar/local_defs.ML Mon Jun 03 15:40:08 2019 +0200
@@ -251,7 +251,7 @@
|> (abs_def o #2 o cert_def ctxt get_pos);
fun prove def_ctxt0 def =
let
- val def_ctxt = Variable.auto_fixes prop def_ctxt0;
+ val def_ctxt = Proof_Context.augment prop def_ctxt0;
val def_thm =
Goal.prove def_ctxt [] [] prop
(fn {context = goal_ctxt, ...} =>
--- a/src/Pure/Isar/proof.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/Pure/Isar/proof.ML Mon Jun 03 15:40:08 2019 +0200
@@ -1093,7 +1093,7 @@
val (propss, binds) =
prep_propp (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) propp;
val goal_ctxt = ctxt
- |> (fold o fold) Variable.auto_fixes propss
+ |> (fold o fold) Proof_Context.augment propss
|> fold Variable.bind_term binds;
fun after_qed' (result_ctxt, results) ctxt' = ctxt'
|> Proof_Context.restore_naming ctxt
--- a/src/Pure/Isar/proof_context.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/Pure/Isar/proof_context.ML Mon Jun 03 15:40:08 2019 +0200
@@ -62,6 +62,7 @@
val facts_of: Proof.context -> Facts.T
val facts_of_fact: Proof.context -> string -> Facts.T
val markup_extern_fact: Proof.context -> string -> Markup.T list * xstring
+ val augment: term -> Proof.context -> Proof.context
val print_name: Proof.context -> string -> string
val pretty_name: Proof.context -> string -> Pretty.T
val pretty_term_abbrev: Proof.context -> term -> Pretty.T
@@ -414,6 +415,14 @@
in (markups, xname) end;
+(* augment context by implicit term declarations *)
+
+fun augment t ctxt = ctxt
+ |> not (Variable.is_body ctxt) ?
+ Variable.add_fixes_direct (rev (Variable.add_free_names ctxt t []))
+ |> Variable.declare_term t;
+
+
(** pretty printing **)
--- a/src/Pure/Isar/specification.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/Pure/Isar/specification.ML Mon Jun 03 15:40:08 2019 +0200
@@ -390,7 +390,7 @@
let
val (stmt, elems_ctxt) = prep_stmt raw_elems raw_stmt ctxt;
val prems = Assumption.local_prems_of elems_ctxt ctxt;
- val stmt_ctxt = fold (fold (Variable.auto_fixes o fst) o snd) stmt elems_ctxt;
+ val stmt_ctxt = fold (fold (Proof_Context.augment o fst) o snd) stmt elems_ctxt;
in
(case raw_stmt of
Element.Shows _ =>
--- a/src/Pure/Thy/document_antiquotations.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML Mon Jun 03 15:40:08 2019 +0200
@@ -43,7 +43,7 @@
handle TYPE _ => err ();
val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
val eq = Logic.mk_equals (t, t');
- val ctxt' = Variable.auto_fixes eq ctxt;
+ val ctxt' = Proof_Context.augment eq ctxt;
in Proof_Context.pretty_term_abbrev ctxt' eq end;
fun pretty_locale ctxt (name, pos) =
--- a/src/Pure/Thy/thy_output.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/Pure/Thy/thy_output.ML Mon Jun 03 15:40:08 2019 +0200
@@ -466,7 +466,7 @@
(* pretty printing *)
fun pretty_term ctxt t =
- Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
+ Syntax.pretty_term (Proof_Context.augment t ctxt) t;
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
--- a/src/Pure/simplifier.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/Pure/simplifier.ML Mon Jun 03 15:40:08 2019 +0200
@@ -126,7 +126,7 @@
fun make_simproc ctxt name {lhss, proc} =
let
- val ctxt' = fold Variable.auto_fixes lhss ctxt;
+ val ctxt' = fold Proof_Context.augment lhss ctxt;
val lhss' = Variable.export_terms ctxt' ctxt lhss;
in
cert_simproc (Proof_Context.theory_of ctxt) name {lhss = lhss', proc = proc}
--- a/src/Pure/variable.ML Mon Jun 03 14:47:27 2019 +0200
+++ b/src/Pure/variable.ML Mon Jun 03 15:40:08 2019 +0200
@@ -58,7 +58,6 @@
val add_fixes_binding: binding list -> Proof.context -> string list * Proof.context
val add_fixes: string list -> Proof.context -> string list * Proof.context
val add_fixes_direct: string list -> Proof.context -> Proof.context
- val auto_fixes: term -> Proof.context -> Proof.context
val fix_dummy_patterns: term -> Proof.context -> term * Proof.context
val variant_fixes: string list -> Proof.context -> string list * Proof.context
val gen_all: Proof.context -> thm -> thm
@@ -476,10 +475,6 @@
|> (snd o add_fixes xs)
|> restore_body ctxt;
-fun auto_fixes t ctxt = ctxt
- |> not (is_body ctxt) ? add_fixes_direct (rev (add_free_names ctxt t []))
- |> declare_term t;
-
(* dummy patterns *)