# HG changeset patch
# User wenzelm
# Date 1559569208 -7200
# Node ID 7f568724d67e17ca205555e03dace3aa10089ac9
# Parent  53d21039518a9f8411356d6fa2d487e5ab768fe2
clarified signature;

diff -r 53d21039518a -r 7f568724d67e src/HOL/Decision_Procs/approximation.ML
--- 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,
diff -r 53d21039518a -r 7f568724d67e src/HOL/Library/old_recdef.ML
--- 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)
diff -r 53d21039518a -r 7f568724d67e src/HOL/Real_Asymp/real_asymp_diag.ML
--- 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
diff -r 53d21039518a -r 7f568724d67e src/HOL/Tools/Function/fun_cases.ML
--- 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
diff -r 53d21039518a -r 7f568724d67e src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- 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 () =>
diff -r 53d21039518a -r 7f568724d67e src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- 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 => []
diff -r 53d21039518a -r 7f568724d67e src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- 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)
diff -r 53d21039518a -r 7f568724d67e src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- 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"
diff -r 53d21039518a -r 7f568724d67e src/HOL/Tools/functor.ML
--- 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);
diff -r 53d21039518a -r 7f568724d67e src/HOL/Tools/inductive.ML
--- 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)
diff -r 53d21039518a -r 7f568724d67e src/HOL/Tools/semiring_normalizer.ML
--- 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;
diff -r 53d21039518a -r 7f568724d67e src/HOL/Tools/value_command.ML
--- 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')]) ();
diff -r 53d21039518a -r 7f568724d67e src/HOL/ex/Commands.thy
--- 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>
 
diff -r 53d21039518a -r 7f568724d67e src/Pure/Isar/element.ML
--- 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
diff -r 53d21039518a -r 7f568724d67e src/Pure/Isar/expression.ML
--- 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;
diff -r 53d21039518a -r 7f568724d67e src/Pure/Isar/isar_cmd.ML
--- 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,
diff -r 53d21039518a -r 7f568724d67e src/Pure/Isar/local_defs.ML
--- 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, ...} =>
diff -r 53d21039518a -r 7f568724d67e src/Pure/Isar/proof.ML
--- 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
diff -r 53d21039518a -r 7f568724d67e src/Pure/Isar/proof_context.ML
--- 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 **)
 
diff -r 53d21039518a -r 7f568724d67e src/Pure/Isar/specification.ML
--- 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 _ =>
diff -r 53d21039518a -r 7f568724d67e src/Pure/Thy/document_antiquotations.ML
--- 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) =
diff -r 53d21039518a -r 7f568724d67e src/Pure/Thy/thy_output.ML
--- 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;
 
diff -r 53d21039518a -r 7f568724d67e src/Pure/simplifier.ML
--- 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}
diff -r 53d21039518a -r 7f568724d67e src/Pure/variable.ML
--- 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 *)