--- a/src/Doc/Isar_Ref/Generic.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy Thu May 25 13:58:46 2023 +0200
@@ -840,9 +840,9 @@
(*<*)experiment begin(*>*)
simproc_setup unit ("x::unit") =
- \<open>fn _ => fn _ => fn ct =>
+ \<open>K (K (fn ct =>
if HOLogic.is_unit (Thm.term_of ct) then NONE
- else SOME (mk_meta_eq @{thm unit_eq})\<close>
+ else SOME (mk_meta_eq @{thm unit_eq})))\<close>
(*<*)end(*>*)
text \<open>
--- a/src/HOL/Bali/Eval.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Bali/Eval.thy Thu May 25 13:58:46 2023 +0200
@@ -851,28 +851,28 @@
by (auto, frule eval_Inj_elim, auto, frule eval_Inj_elim, auto)
simproc_setup eval_expr ("G\<turnstile>s \<midarrow>In1l t\<succ>\<rightarrow> (w, s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
- | _ => SOME (mk_meta_eq @{thm eval_expr_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm eval_expr_eq}))))\<close>
simproc_setup eval_var ("G\<turnstile>s \<midarrow>In2 t\<succ>\<rightarrow> (w, s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
- | _ => SOME (mk_meta_eq @{thm eval_var_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm eval_var_eq}))))\<close>
simproc_setup eval_exprs ("G\<turnstile>s \<midarrow>In3 t\<succ>\<rightarrow> (w, s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
- | _ => SOME (mk_meta_eq @{thm eval_exprs_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm eval_exprs_eq}))))\<close>
simproc_setup eval_stmt ("G\<turnstile>s \<midarrow>In1r t\<succ>\<rightarrow> (w, s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
- | _ => SOME (mk_meta_eq @{thm eval_stmt_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm eval_stmt_eq}))))\<close>
ML \<open>
ML_Thms.bind_thms ("AbruptIs", sum3_instantiate \<^context> @{thm eval.Abrupt})
@@ -947,10 +947,10 @@
done
simproc_setup eval_no_abrupt ("G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ (Const (\<^const_name>\<open>Pair\<close>, _) $ (Const (\<^const_name>\<open>None\<close>, _)) $ _) $ _ $ _ $ _) => NONE
- | _ => SOME (mk_meta_eq @{thm eval_no_abrupt}))
+ | _ => SOME (mk_meta_eq @{thm eval_no_abrupt}))))
\<close>
@@ -967,10 +967,10 @@
done
simproc_setup eval_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ _ $ (Const (\<^const_name>\<open>Pair\<close>, _) $ (Const (\<^const_name>\<open>Some\<close>, _) $ _)$ _)) => NONE
- | _ => SOME (mk_meta_eq @{thm eval_abrupt}))
+ | _ => SOME (mk_meta_eq @{thm eval_abrupt}))))
\<close>
lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else undefined)\<rightarrow> s"
--- a/src/HOL/Bali/Evaln.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Bali/Evaln.thy Thu May 25 13:58:46 2023 +0200
@@ -269,28 +269,28 @@
by (auto, frule evaln_Inj_elim, auto, frule evaln_Inj_elim, auto)
simproc_setup evaln_expr ("G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
- | _ => SOME (mk_meta_eq @{thm evaln_expr_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm evaln_expr_eq}))))\<close>
simproc_setup evaln_var ("G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
- | _ => SOME (mk_meta_eq @{thm evaln_var_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm evaln_var_eq}))))\<close>
simproc_setup evaln_exprs ("G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
- | _ => SOME (mk_meta_eq @{thm evaln_exprs_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm evaln_exprs_eq}))))\<close>
simproc_setup evaln_stmt ("G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
- | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq}))))\<close>
ML \<open>ML_Thms.bind_thms ("evaln_AbruptIs", sum3_instantiate \<^context> @{thm evaln.Abrupt})\<close>
declare evaln_AbruptIs [intro!]
@@ -356,11 +356,11 @@
done
simproc_setup evaln_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ _ $ _ $ (Const (\<^const_name>\<open>Pair\<close>, _) $ (Const (\<^const_name>\<open>Some\<close>,_) $ _)$ _))
=> NONE
- | _ => SOME (mk_meta_eq @{thm evaln_abrupt}))
+ | _ => SOME (mk_meta_eq @{thm evaln_abrupt}))))
\<close>
lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else undefined)\<midarrow>n\<rightarrow> s"
--- a/src/HOL/Bali/WellType.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Bali/WellType.thy Thu May 25 13:58:46 2023 +0200
@@ -605,28 +605,28 @@
by (auto, frule wt_Inj_elim, auto, frule wt_Inj_elim, auto)
simproc_setup wt_expr ("E,dt\<Turnstile>In1l t\<Colon>U") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
- | _ => SOME (mk_meta_eq @{thm wt_expr_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm wt_expr_eq}))))\<close>
simproc_setup wt_var ("E,dt\<Turnstile>In2 t\<Colon>U") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
- | _ => SOME (mk_meta_eq @{thm wt_var_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm wt_var_eq}))))\<close>
simproc_setup wt_exprs ("E,dt\<Turnstile>In3 t\<Colon>U") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
- | _ => SOME (mk_meta_eq @{thm wt_exprs_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm wt_exprs_eq}))))\<close>
simproc_setup wt_stmt ("E,dt\<Turnstile>In1r t\<Colon>U") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
(_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
- | _ => SOME (mk_meta_eq @{thm wt_stmt_eq}))\<close>
+ | _ => SOME (mk_meta_eq @{thm wt_stmt_eq}))))\<close>
lemma wt_elim_BinOp:
"\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T;
--- a/src/HOL/Boolean_Algebras.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Boolean_Algebras.thy Thu May 25 13:58:46 2023 +0200
@@ -513,10 +513,10 @@
ML_file \<open>Tools/boolean_algebra_cancel.ML\<close>
simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") =
- \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_sup_conv\<close>
+ \<open>K (K (try Boolean_Algebra_Cancel.cancel_sup_conv))\<close>
simproc_setup boolean_algebra_cancel_inf ("inf a b::'a::boolean_algebra") =
- \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_inf_conv\<close>
+ \<open>K (K (try Boolean_Algebra_Cancel.cancel_inf_conv))\<close>
context boolean_algebra
--- a/src/HOL/Data_Structures/Less_False.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Data_Structures/Less_False.thy Thu May 25 13:58:46 2023 +0200
@@ -6,7 +6,7 @@
imports Main
begin
-simproc_setup less_False ("(x::'a::order) < y") = \<open>fn _ => fn ctxt => fn ct =>
+simproc_setup less_False ("(x::'a::order) < y") = \<open>K (fn ctxt => fn ct =>
let
fun prp t thm = Thm.full_prop_of thm aconv t;
@@ -25,7 +25,7 @@
end
| SOME thm => NONE
end;
- in prove_less_False (Thm.term_of ct) end
+ in prove_less_False (Thm.term_of ct) end)
\<close>
end
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Thu May 25 13:58:46 2023 +0200
@@ -942,16 +942,15 @@
context cring
begin
-local_setup \<open>
-Local_Theory.declaration {syntax = false, pervasive = false}
- (fn phi => Ring_Tac.Ring_Simps.map (Ring_Tac.insert_rules Ring_Tac.eq_ring_simps
+declaration \<open>fn phi =>
+ Ring_Tac.Ring_Simps.map (Ring_Tac.insert_rules Ring_Tac.eq_ring_simps
(Morphism.term phi \<^term>\<open>R\<close>,
(Morphism.fact phi @{thms Ipol.simps [meta] Ipol_Pc [meta]},
Morphism.fact phi @{thms Ipolex.simps [meta] Ipolex_Const [meta]},
Morphism.fact phi @{thms Ipolex_polex_list.simps [meta]},
Morphism.fact phi @{thms in_carrier_Nil in_carrier_Cons},
singleton (Morphism.fact phi) @{thm head.simps(2) [meta]},
- singleton (Morphism.fact phi) @{thm norm_subst_correct [meta]}))))
+ singleton (Morphism.fact phi) @{thm norm_subst_correct [meta]})))
\<close>
end
--- a/src/HOL/Decision_Procs/Conversions.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Decision_Procs/Conversions.thy Thu May 25 13:58:46 2023 +0200
@@ -20,7 +20,7 @@
\<close>
attribute_setup meta =
- \<open>Scan.succeed (fn (ctxt, th) => (NONE, SOME (mk_meta_eq th)))\<close>
+ \<open>Scan.succeed (Thm.rule_attribute [] (K mk_meta_eq))\<close>
\<open>convert equality to meta equality\<close>
ML \<open>
--- a/src/HOL/Decision_Procs/Reflective_Field.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy Thu May 25 13:58:46 2023 +0200
@@ -909,15 +909,14 @@
context field
begin
-local_setup \<open>
-Local_Theory.declaration {syntax = false, pervasive = false}
- (fn phi => Field_Tac.Field_Simps.map (Ring_Tac.insert_rules Field_Tac.eq_field_simps
+declaration \<open>fn phi =>
+ Field_Tac.Field_Simps.map (Ring_Tac.insert_rules Field_Tac.eq_field_simps
(Morphism.term phi \<^term>\<open>R\<close>,
(Morphism.fact phi @{thms feval.simps [meta] feval_Cnst [meta]},
Morphism.fact phi @{thms peval.simps [meta] peval_Cnst [meta]},
Morphism.fact phi @{thms nonzero.simps [meta] nonzero_singleton [meta]},
singleton (Morphism.fact phi) @{thm nth_el_Cons [meta]},
- singleton (Morphism.fact phi) @{thm feval_eq}))))
+ singleton (Morphism.fact phi) @{thm feval_eq})))
\<close>
end
--- a/src/HOL/Eisbach/Tests.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Eisbach/Tests.thy Thu May 25 13:58:46 2023 +0200
@@ -432,9 +432,7 @@
assumes A : "A"
begin
-local_setup
- \<open>Local_Theory.declaration {pervasive = false, syntax = false}
- (fn phi => Data.put (Morphism.fact phi @{thms A}))\<close>
+declaration \<open>fn phi => Data.put (Morphism.fact phi @{thms A})\<close>
lemma A by dynamic_thms_test
--- a/src/HOL/Eisbach/method_closure.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Eisbach/method_closure.ML Thu May 25 13:58:46 2023 +0200
@@ -66,13 +66,14 @@
let
val name = Local_Theory.full_name lthy binding;
in
- lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
- Data.map
- (Symtab.update (name,
- {vars = map (Morphism.term phi) (#vars closure),
- named_thms = #named_thms closure,
- methods = #methods closure,
- body = (Method.map_source o map) (Token.transform phi) (#body closure)})))
+ lthy |> Local_Theory.declaration {syntax = false, pervasive = true, pos = Binding.pos_of binding}
+ (fn phi =>
+ Data.map
+ (Symtab.update (name,
+ {vars = map (Morphism.term phi) (#vars closure),
+ named_thms = #named_thms closure,
+ methods = #methods closure,
+ body = (Method.map_source o map) (Token.transform phi) (#body closure)})))
end;
--- a/src/HOL/Enum.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Enum.thy Thu May 25 13:58:46 2023 +0200
@@ -564,10 +564,10 @@
by(cases x) simp
simproc_setup finite_1_eq ("x::finite_1") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
(case Thm.term_of ct of
Const (\<^const_name>\<open>a\<^sub>1\<close>, _) => NONE
- | _ => SOME (mk_meta_eq @{thm finite_1_eq}))
+ | _ => SOME (mk_meta_eq @{thm finite_1_eq}))))
\<close>
instantiation finite_1 :: complete_boolean_algebra
--- a/src/HOL/Finite_Set.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Finite_Set.thy Thu May 25 13:58:46 2023 +0200
@@ -193,7 +193,7 @@
lemma finite_subset: "A \<subseteq> B \<Longrightarrow> finite B \<Longrightarrow> finite A"
by (rule rev_finite_subset)
-simproc_setup finite ("finite A") = \<open>fn _ =>
+simproc_setup finite ("finite A") = \<open>
let
val finite_subset = @{thm finite_subset}
val Eq_TrueI = @{thm Eq_TrueI}
@@ -209,17 +209,17 @@
fun comb (A,sub_th) (A',fin_th) ths = if A aconv A' then (sub_th,fin_th) :: ths else ths
- fun proc ss ct =
+ fun proc ctxt ct =
(let
val _ $ A = Thm.term_of ct
- val prems = Simplifier.prems_of ss
+ val prems = Simplifier.prems_of ctxt
val fins = map_filter is_finite prems
val subsets = map_filter (is_subset A) prems
in case fold_product comb subsets fins [] of
(sub_th,fin_th) :: _ => SOME((fin_th RS (sub_th RS finite_subset)) RS Eq_TrueI)
| _ => NONE
end)
-in proc end
+in K proc end
\<close>
(* Needs to be used with care *)
--- a/src/HOL/Fun.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Fun.thy Thu May 25 13:58:46 2023 +0200
@@ -1353,7 +1353,7 @@
text \<open>Simplify terms of the form \<open>f(\<dots>,x:=y,\<dots>,x:=z,\<dots>)\<close> to \<open>f(\<dots>,x:=z,\<dots>)\<close>\<close>
-simproc_setup fun_upd2 ("f(v := w, x := y)") = \<open>fn _ =>
+simproc_setup fun_upd2 ("f(v := w, x := y)") = \<open>
let
fun gen_fun_upd NONE T _ _ = NONE
| gen_fun_upd (SOME f) T x y = SOME (Const (\<^const_name>\<open>fun_upd\<close>, T) $ f $ x $ y)
@@ -1380,7 +1380,7 @@
resolve_tac ctxt @{thms ext} 1 THEN
simp_tac (put_simpset ss ctxt) 1)))
end
- in proc end
+ in K proc end
\<close>
--- a/src/HOL/Groups.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Groups.thy Thu May 25 13:58:46 2023 +0200
@@ -178,8 +178,8 @@
| _ => false)
\<close>
-simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
-simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
+simproc_setup reorient_zero ("0 = x") = \<open>K Reorient_Proc.proc\<close>
+simproc_setup reorient_one ("1 = x") = \<open>K Reorient_Proc.proc\<close>
typed_print_translation \<open>
let
--- a/src/HOL/HOL.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/HOL.thy Thu May 25 13:58:46 2023 +0200
@@ -1236,7 +1236,7 @@
text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close>
-simproc_setup neq ("x = y") = \<open>fn _ =>
+simproc_setup neq ("x = y") = \<open>
let
val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI};
fun is_neq eq lhs rhs thm =
@@ -1252,7 +1252,7 @@
SOME thm => SOME (thm RS neq_to_EQ_False)
| NONE => NONE)
| _ => NONE);
- in proc end
+ in K proc end
\<close>
simproc_setup let_simp ("Let x f") = \<open>
@@ -1266,7 +1266,7 @@
Abs (_, _, t') => count_loose t' 0 <= 1
| _ => true);
in
- fn _ => fn ctxt => fn ct =>
+ K (fn ctxt => fn ct =>
if is_trivial_let (Thm.term_of ct)
then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
else
@@ -1308,7 +1308,7 @@
in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
end
| _ => NONE)
- end
+ end)
end
\<close>
@@ -1649,7 +1649,7 @@
signature REORIENT_PROC =
sig
val add : (term -> bool) -> theory -> theory
- val proc : morphism -> Proof.context -> cterm -> thm option
+ val proc : Proof.context -> cterm -> thm option
end;
structure Reorient_Proc : REORIENT_PROC =
@@ -1664,7 +1664,7 @@
fun matches thy t = exists (fn (m, _) => m t) (Data.get thy);
val meta_reorient = @{thm eq_commute [THEN eq_reflection]};
- fun proc phi ctxt ct =
+ fun proc ctxt ct =
let
val thy = Proof_Context.theory_of ctxt;
in
@@ -1851,12 +1851,12 @@
declare [[coercion_args NO_MATCH - -]]
-simproc_setup NO_MATCH ("NO_MATCH pat val") = \<open>fn _ => fn ctxt => fn ct =>
+simproc_setup NO_MATCH ("NO_MATCH pat val") = \<open>K (fn ctxt => fn ct =>
let
val thy = Proof_Context.theory_of ctxt
val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)
val m = Pattern.matches thy (dest_binop (Thm.term_of ct))
- in if m then NONE else SOME @{thm NO_MATCH_def} end
+ in if m then NONE else SOME @{thm NO_MATCH_def} end)
\<close>
text \<open>
--- a/src/HOL/HOLCF/Cfun.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/HOLCF/Cfun.thy Thu May 25 13:58:46 2023 +0200
@@ -142,14 +142,14 @@
\<close>
simproc_setup beta_cfun_proc ("Rep_cfun (Abs_cfun f)") = \<open>
- fn phi => fn ctxt => fn ct =>
+ K (fn ctxt => fn ct =>
let
val f = #2 (Thm.dest_comb (#2 (Thm.dest_comb ct)));
val [T, U] = Thm.dest_ctyp (Thm.ctyp_of_cterm f);
val tr = Thm.instantiate' [SOME T, SOME U] [SOME f] (mk_meta_eq @{thm Abs_cfun_inverse2});
val rules = Named_Theorems.get ctxt \<^named_theorems>\<open>cont2cont\<close>;
val tac = SOLVED' (REPEAT_ALL_NEW (match_tac ctxt (rev rules)));
- in SOME (perhaps (SINGLE (tac 1)) tr) end
+ in SOME (perhaps (SINGLE (tac 1)) tr) end)
\<close>
text \<open>Eta-equality for continuous functions\<close>
--- a/src/HOL/HOLCF/Pcpo.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/HOLCF/Pcpo.thy Thu May 25 13:58:46 2023 +0200
@@ -157,7 +157,7 @@
text \<open>Simproc to rewrite \<^term>\<open>\<bottom> = x\<close> to \<^term>\<open>x = \<bottom>\<close>.\<close>
setup \<open>Reorient_Proc.add (fn \<^Const_>\<open>bottom _\<close> => true | _ => false)\<close>
-simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc
+simproc_setup reorient_bottom ("\<bottom> = x") = \<open>K Reorient_Proc.proc\<close>
text \<open>useful lemmas about \<^term>\<open>\<bottom>\<close>\<close>
--- a/src/HOL/HOLCF/Tools/fixrec.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Thu May 25 13:58:46 2023 +0200
@@ -171,7 +171,7 @@
fun unfold_note (name, thm) : Attrib.binding * Thm.thm list =
let
val thm_name = Binding.qualify true name (Binding.name "unfold")
- val src = Attrib.internal (K add_unfold)
+ val src = Attrib.internal \<^here> (K add_unfold)
in
((thm_name, [src]), [thm])
end
--- a/src/HOL/Library/Extended_Nat.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Library/Extended_Nat.thy Thu May 25 13:58:46 2023 +0200
@@ -588,15 +588,15 @@
simproc_setup enat_eq_cancel
("(l::enat) + m = n" | "(l::enat) = m + n") =
- \<open>fn phi => fn ctxt => fn ct => Eq_Enat_Cancel.proc ctxt (Thm.term_of ct)\<close>
+ \<open>K (fn ctxt => fn ct => Eq_Enat_Cancel.proc ctxt (Thm.term_of ct))\<close>
simproc_setup enat_le_cancel
("(l::enat) + m \<le> n" | "(l::enat) \<le> m + n") =
- \<open>fn phi => fn ctxt => fn ct => Le_Enat_Cancel.proc ctxt (Thm.term_of ct)\<close>
+ \<open>K (fn ctxt => fn ct => Le_Enat_Cancel.proc ctxt (Thm.term_of ct))\<close>
simproc_setup enat_less_cancel
("(l::enat) + m < n" | "(l::enat) < m + n") =
- \<open>fn phi => fn ctxt => fn ct => Less_Enat_Cancel.proc ctxt (Thm.term_of ct)\<close>
+ \<open>K (fn ctxt => fn ct => Less_Enat_Cancel.proc ctxt (Thm.term_of ct))\<close>
text \<open>TODO: add regression tests for these simprocs\<close>
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Thu May 25 13:58:46 2023 +0200
@@ -433,15 +433,15 @@
simproc_setup ennreal_eq_cancel
("(l::ennreal) + m = n" | "(l::ennreal) = m + n") =
- \<open>fn phi => fn ctxt => fn ct => Eq_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
+ \<open>K (fn ctxt => fn ct => Eq_Ennreal_Cancel.proc ctxt (Thm.term_of ct))\<close>
simproc_setup ennreal_le_cancel
("(l::ennreal) + m \<le> n" | "(l::ennreal) \<le> m + n") =
- \<open>fn phi => fn ctxt => fn ct => Le_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
+ \<open>K (fn ctxt => fn ct => Le_Ennreal_Cancel.proc ctxt (Thm.term_of ct))\<close>
simproc_setup ennreal_less_cancel
("(l::ennreal) + m < n" | "(l::ennreal) < m + n") =
- \<open>fn phi => fn ctxt => fn ct => Less_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
+ \<open>K (fn ctxt => fn ct => Less_Ennreal_Cancel.proc ctxt (Thm.term_of ct))\<close>
subsection \<open>Order with top\<close>
--- a/src/HOL/Library/Multiset.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Library/Multiset.thy Thu May 25 13:58:46 2023 +0200
@@ -1003,28 +1003,28 @@
"add_mset a m = n" | "m = add_mset a n" |
"replicate_mset p a = n" | "m = replicate_mset p a" |
"repeat_mset p m = n" | "m = repeat_mset p m") =
- \<open>fn phi => Cancel_Simprocs.eq_cancel\<close>
+ \<open>K Cancel_Simprocs.eq_cancel\<close>
simproc_setup msetsubset_cancel
("(l::'a multiset) + m \<subset># n" | "(l::'a multiset) \<subset># m + n" |
"add_mset a m \<subset># n" | "m \<subset># add_mset a n" |
"replicate_mset p r \<subset># n" | "m \<subset># replicate_mset p r" |
"repeat_mset p m \<subset># n" | "m \<subset># repeat_mset p m") =
- \<open>fn phi => Multiset_Simprocs.subset_cancel_msets\<close>
+ \<open>K Multiset_Simprocs.subset_cancel_msets\<close>
simproc_setup msetsubset_eq_cancel
("(l::'a multiset) + m \<subseteq># n" | "(l::'a multiset) \<subseteq># m + n" |
"add_mset a m \<subseteq># n" | "m \<subseteq># add_mset a n" |
"replicate_mset p r \<subseteq># n" | "m \<subseteq># replicate_mset p r" |
"repeat_mset p m \<subseteq># n" | "m \<subseteq># repeat_mset p m") =
- \<open>fn phi => Multiset_Simprocs.subseteq_cancel_msets\<close>
+ \<open>K Multiset_Simprocs.subseteq_cancel_msets\<close>
simproc_setup msetdiff_cancel
("((l::'a multiset) + m) - n" | "(l::'a multiset) - (m + n)" |
"add_mset a m - n" | "m - add_mset a n" |
"replicate_mset p r - n" | "m - replicate_mset p r" |
"repeat_mset p m - n" | "m - repeat_mset p m") =
- \<open>fn phi => Cancel_Simprocs.diff_cancel\<close>
+ \<open>K Cancel_Simprocs.diff_cancel\<close>
subsubsection \<open>Conditionally complete lattice\<close>
--- a/src/HOL/Library/Multiset_Order.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Library/Multiset_Order.thy Thu May 25 13:58:46 2023 +0200
@@ -776,14 +776,14 @@
"add_mset a m < n" | "m < add_mset a n" |
"replicate_mset p a < n" | "m < replicate_mset p a" |
"repeat_mset p m < n" | "m < repeat_mset p n") =
- \<open>fn phi => Cancel_Simprocs.less_cancel\<close>
+ \<open>K Cancel_Simprocs.less_cancel\<close>
simproc_setup msetle_cancel
("(l::'a::preorder multiset) + m \<le> n" | "(l::'a multiset) \<le> m + n" |
"add_mset a m \<le> n" | "m \<le> add_mset a n" |
"replicate_mset p a \<le> n" | "m \<le> replicate_mset p a" |
"repeat_mset p m \<le> n" | "m \<le> repeat_mset p n") =
- \<open>fn phi => Cancel_Simprocs.less_eq_cancel\<close>
+ \<open>K Cancel_Simprocs.less_eq_cancel\<close>
subsection \<open>Additional facts and instantiations\<close>
--- a/src/HOL/Library/adhoc_overloading.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Library/adhoc_overloading.ML Thu May 25 13:58:46 2023 +0200
@@ -227,7 +227,7 @@
|> map (apfst (const_name lthy))
|> map (apsnd (map (read_term lthy)));
in
- Local_Theory.declaration {syntax = true, pervasive = false}
+ Local_Theory.declaration {syntax = true, pervasive = false, pos = Position.thread_data ()}
(adhoc_overloading_cmd' add args) lthy
end;
--- a/src/HOL/List.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/List.thy Thu May 25 13:58:46 2023 +0200
@@ -1045,7 +1045,7 @@
else if lastl aconv lastr then rearr @{thm append_same_eq}
else NONE
end;
- in fn _ => fn ctxt => fn ct => list_eq ctxt (Thm.term_of ct) end
+ in K (fn ctxt => fn ct => list_eq ctxt (Thm.term_of ct)) end
\<close>
--- a/src/HOL/Nat.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Nat.thy Thu May 25 13:58:46 2023 +0200
@@ -1968,19 +1968,19 @@
simproc_setup nateq_cancel_sums
("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
- \<open>fn phi => try o Nat_Arith.cancel_eq_conv\<close>
+ \<open>K (try o Nat_Arith.cancel_eq_conv)\<close>
simproc_setup natless_cancel_sums
("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") =
- \<open>fn phi => try o Nat_Arith.cancel_less_conv\<close>
+ \<open>K (try o Nat_Arith.cancel_less_conv)\<close>
simproc_setup natle_cancel_sums
("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") =
- \<open>fn phi => try o Nat_Arith.cancel_le_conv\<close>
+ \<open>K (try o Nat_Arith.cancel_le_conv)\<close>
simproc_setup natdiff_cancel_sums
("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
- \<open>fn phi => try o Nat_Arith.cancel_diff_conv\<close>
+ \<open>K (try o Nat_Arith.cancel_diff_conv)\<close>
context order
begin
--- a/src/HOL/Nominal/nominal_inductive.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Thu May 25 13:58:46 2023 +0200
@@ -566,7 +566,7 @@
val strong_cases = map (mk_cases_proof ##> Inductive.rulify lthy1)
(thsss ~~ elims ~~ cases_prems ~~ cases_prems');
val strong_induct_atts =
- map (Attrib.internal o K)
+ map (Attrib.internal \<^here> o K)
[ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of strong_raw_induct))];
val strong_induct =
if length names > 1 then strong_raw_induct
@@ -580,12 +580,12 @@
Local_Theory.notes
[((rec_qualified (Binding.name "strong_inducts"), []),
strong_inducts |> map (fn th => ([th],
- [Attrib.internal (K ind_case_names),
- Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th)))])))] |> snd |>
+ [Attrib.internal \<^here> (K ind_case_names),
+ Attrib.internal \<^here> (K (Rule_Cases.consumes (1 - Thm.nprems_of th)))])))] |> snd |>
Local_Theory.notes (map (fn ((name, elim), (_, cases)) =>
((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
- [Attrib.internal (K (Rule_Cases.case_names (map snd cases))),
- Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of elim)))]), [([elim], [])]))
+ [Attrib.internal \<^here> (K (Rule_Cases.case_names (map snd cases))),
+ Attrib.internal \<^here> (K (Rule_Cases.consumes (1 - Thm.nprems_of elim)))]), [([elim], [])]))
(strong_cases ~~ induct_cases')) |> snd
end)
(map (map (rulify_term thy #> rpair [])) vc_compat)
@@ -675,7 +675,7 @@
lthy |>
Local_Theory.notes (map (fn (name, ths) =>
((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
- [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
+ @{attributes [eqvt]}), [(ths, [])]))
(names ~~ transp thss)) |> snd
end;
--- a/src/HOL/Nominal/nominal_inductive2.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Thu May 25 13:58:46 2023 +0200
@@ -466,7 +466,7 @@
val strong_raw_induct =
mk_ind_proof lthy1 thss' |> Inductive.rulify lthy1;
val strong_induct_atts =
- map (Attrib.internal o K)
+ map (Attrib.internal \<^here> o K)
[ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of strong_raw_induct))];
val strong_induct =
if length names > 1 then strong_raw_induct
@@ -484,8 +484,8 @@
lthy2 |>
Local_Theory.notes [((inducts_name, []),
strong_inducts |> map (fn th => ([th],
- [Attrib.internal (K ind_case_names),
- Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th)))])))] |> snd
+ [Attrib.internal \<^here> (K ind_case_names),
+ Attrib.internal \<^here> (K (Rule_Cases.consumes (1 - Thm.nprems_of th)))])))] |> snd
end)
(map (map (rulify_term thy #> rpair [])) vc_compat)
end;
--- a/src/HOL/Nonstandard_Analysis/NSA.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Nonstandard_Analysis/NSA.thy Thu May 25 13:58:46 2023 +0200
@@ -549,12 +549,12 @@
("0 \<approx> x" | "1 \<approx> y" | "numeral w \<approx> z" | "- 1 \<approx> y" | "- numeral w \<approx> r") =
\<open>
let val rule = @{thm approx_reorient} RS eq_reflection
- fun proc phi ss ct =
+ fun proc ct =
case Thm.term_of ct of
_ $ t $ u => if can HOLogic.dest_number u then NONE
else if can HOLogic.dest_number t then SOME rule else NONE
| _ => NONE
- in proc end
+ in K (K proc) end
\<close>
lemma Infinitesimal_approx_minus: "x - y \<in> Infinitesimal \<longleftrightarrow> x \<approx> y"
--- a/src/HOL/Num.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Num.thy Thu May 25 13:58:46 2023 +0200
@@ -1394,7 +1394,7 @@
\<close>
simproc_setup reorient_numeral ("numeral w = x" | "- numeral w = y") =
- Reorient_Proc.proc
+ \<open>K Reorient_Proc.proc\<close>
subsubsection \<open>Simplification of arithmetic operations on integer constants\<close>
--- a/src/HOL/Numeral_Simprocs.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Numeral_Simprocs.thy Thu May 25 13:58:46 2023 +0200
@@ -104,17 +104,17 @@
simproc_setup semiring_assoc_fold
("(a::'a::comm_semiring_1_cancel) * b") =
- \<open>fn phi => Numeral_Simprocs.assoc_fold\<close>
+ \<open>K Numeral_Simprocs.assoc_fold\<close>
(* TODO: see whether the type class can be generalized further *)
simproc_setup int_combine_numerals
("(i::'a::comm_ring_1) + j" | "(i::'a::comm_ring_1) - j") =
- \<open>fn phi => Numeral_Simprocs.combine_numerals\<close>
+ \<open>K Numeral_Simprocs.combine_numerals\<close>
simproc_setup field_combine_numerals
("(i::'a::{field,ring_char_0}) + j"
|"(i::'a::{field,ring_char_0}) - j") =
- \<open>fn phi => Numeral_Simprocs.field_combine_numerals\<close>
+ \<open>K Numeral_Simprocs.field_combine_numerals\<close>
simproc_setup inteq_cancel_numerals
("(l::'a::comm_ring_1) + m = n"
@@ -125,7 +125,7 @@
|"(l::'a::comm_ring_1) = m * n"
|"- (l::'a::comm_ring_1) = m"
|"(l::'a::comm_ring_1) = - m") =
- \<open>fn phi => Numeral_Simprocs.eq_cancel_numerals\<close>
+ \<open>K Numeral_Simprocs.eq_cancel_numerals\<close>
simproc_setup intless_cancel_numerals
("(l::'a::linordered_idom) + m < n"
@@ -136,7 +136,7 @@
|"(l::'a::linordered_idom) < m * n"
|"- (l::'a::linordered_idom) < m"
|"(l::'a::linordered_idom) < - m") =
- \<open>fn phi => Numeral_Simprocs.less_cancel_numerals\<close>
+ \<open>K Numeral_Simprocs.less_cancel_numerals\<close>
simproc_setup intle_cancel_numerals
("(l::'a::linordered_idom) + m \<le> n"
@@ -147,138 +147,138 @@
|"(l::'a::linordered_idom) \<le> m * n"
|"- (l::'a::linordered_idom) \<le> m"
|"(l::'a::linordered_idom) \<le> - m") =
- \<open>fn phi => Numeral_Simprocs.le_cancel_numerals\<close>
+ \<open>K Numeral_Simprocs.le_cancel_numerals\<close>
simproc_setup ring_eq_cancel_numeral_factor
("(l::'a::{idom,ring_char_0}) * m = n"
|"(l::'a::{idom,ring_char_0}) = m * n") =
- \<open>fn phi => Numeral_Simprocs.eq_cancel_numeral_factor\<close>
+ \<open>K Numeral_Simprocs.eq_cancel_numeral_factor\<close>
simproc_setup ring_less_cancel_numeral_factor
("(l::'a::linordered_idom) * m < n"
|"(l::'a::linordered_idom) < m * n") =
- \<open>fn phi => Numeral_Simprocs.less_cancel_numeral_factor\<close>
+ \<open>K Numeral_Simprocs.less_cancel_numeral_factor\<close>
simproc_setup ring_le_cancel_numeral_factor
("(l::'a::linordered_idom) * m <= n"
|"(l::'a::linordered_idom) <= m * n") =
- \<open>fn phi => Numeral_Simprocs.le_cancel_numeral_factor\<close>
+ \<open>K Numeral_Simprocs.le_cancel_numeral_factor\<close>
(* TODO: remove comm_ring_1 constraint if possible *)
simproc_setup int_div_cancel_numeral_factors
("((l::'a::{euclidean_semiring_cancel,comm_ring_1,ring_char_0}) * m) div n"
|"(l::'a::{euclidean_semiring_cancel,comm_ring_1,ring_char_0}) div (m * n)") =
- \<open>fn phi => Numeral_Simprocs.div_cancel_numeral_factor\<close>
+ \<open>K Numeral_Simprocs.div_cancel_numeral_factor\<close>
simproc_setup divide_cancel_numeral_factor
("((l::'a::{field,ring_char_0}) * m) / n"
|"(l::'a::{field,ring_char_0}) / (m * n)"
|"((numeral v)::'a::{field,ring_char_0}) / (numeral w)") =
- \<open>fn phi => Numeral_Simprocs.divide_cancel_numeral_factor\<close>
+ \<open>K Numeral_Simprocs.divide_cancel_numeral_factor\<close>
simproc_setup ring_eq_cancel_factor
("(l::'a::idom) * m = n" | "(l::'a::idom) = m * n") =
- \<open>fn phi => Numeral_Simprocs.eq_cancel_factor\<close>
+ \<open>K Numeral_Simprocs.eq_cancel_factor\<close>
simproc_setup linordered_ring_le_cancel_factor
("(l::'a::linordered_idom) * m <= n"
|"(l::'a::linordered_idom) <= m * n") =
- \<open>fn phi => Numeral_Simprocs.le_cancel_factor\<close>
+ \<open>K Numeral_Simprocs.le_cancel_factor\<close>
simproc_setup linordered_ring_less_cancel_factor
("(l::'a::linordered_idom) * m < n"
|"(l::'a::linordered_idom) < m * n") =
- \<open>fn phi => Numeral_Simprocs.less_cancel_factor\<close>
+ \<open>K Numeral_Simprocs.less_cancel_factor\<close>
simproc_setup int_div_cancel_factor
("((l::'a::euclidean_semiring_cancel) * m) div n"
|"(l::'a::euclidean_semiring_cancel) div (m * n)") =
- \<open>fn phi => Numeral_Simprocs.div_cancel_factor\<close>
+ \<open>K Numeral_Simprocs.div_cancel_factor\<close>
simproc_setup int_mod_cancel_factor
("((l::'a::euclidean_semiring_cancel) * m) mod n"
|"(l::'a::euclidean_semiring_cancel) mod (m * n)") =
- \<open>fn phi => Numeral_Simprocs.mod_cancel_factor\<close>
+ \<open>K Numeral_Simprocs.mod_cancel_factor\<close>
simproc_setup dvd_cancel_factor
("((l::'a::idom) * m) dvd n"
|"(l::'a::idom) dvd (m * n)") =
- \<open>fn phi => Numeral_Simprocs.dvd_cancel_factor\<close>
+ \<open>K Numeral_Simprocs.dvd_cancel_factor\<close>
simproc_setup divide_cancel_factor
("((l::'a::field) * m) / n"
|"(l::'a::field) / (m * n)") =
- \<open>fn phi => Numeral_Simprocs.divide_cancel_factor\<close>
+ \<open>K Numeral_Simprocs.divide_cancel_factor\<close>
ML_file \<open>Tools/nat_numeral_simprocs.ML\<close>
simproc_setup nat_combine_numerals
("(i::nat) + j" | "Suc (i + j)") =
- \<open>fn phi => Nat_Numeral_Simprocs.combine_numerals\<close>
+ \<open>K Nat_Numeral_Simprocs.combine_numerals\<close>
simproc_setup nateq_cancel_numerals
("(l::nat) + m = n" | "(l::nat) = m + n" |
"(l::nat) * m = n" | "(l::nat) = m * n" |
"Suc m = n" | "m = Suc n") =
- \<open>fn phi => Nat_Numeral_Simprocs.eq_cancel_numerals\<close>
+ \<open>K Nat_Numeral_Simprocs.eq_cancel_numerals\<close>
simproc_setup natless_cancel_numerals
("(l::nat) + m < n" | "(l::nat) < m + n" |
"(l::nat) * m < n" | "(l::nat) < m * n" |
"Suc m < n" | "m < Suc n") =
- \<open>fn phi => Nat_Numeral_Simprocs.less_cancel_numerals\<close>
+ \<open>K Nat_Numeral_Simprocs.less_cancel_numerals\<close>
simproc_setup natle_cancel_numerals
("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" |
"(l::nat) * m \<le> n" | "(l::nat) \<le> m * n" |
"Suc m \<le> n" | "m \<le> Suc n") =
- \<open>fn phi => Nat_Numeral_Simprocs.le_cancel_numerals\<close>
+ \<open>K Nat_Numeral_Simprocs.le_cancel_numerals\<close>
simproc_setup natdiff_cancel_numerals
("((l::nat) + m) - n" | "(l::nat) - (m + n)" |
"(l::nat) * m - n" | "(l::nat) - m * n" |
"Suc m - n" | "m - Suc n") =
- \<open>fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals\<close>
+ \<open>K Nat_Numeral_Simprocs.diff_cancel_numerals\<close>
simproc_setup nat_eq_cancel_numeral_factor
("(l::nat) * m = n" | "(l::nat) = m * n") =
- \<open>fn phi => Nat_Numeral_Simprocs.eq_cancel_numeral_factor\<close>
+ \<open>K Nat_Numeral_Simprocs.eq_cancel_numeral_factor\<close>
simproc_setup nat_less_cancel_numeral_factor
("(l::nat) * m < n" | "(l::nat) < m * n") =
- \<open>fn phi => Nat_Numeral_Simprocs.less_cancel_numeral_factor\<close>
+ \<open>K Nat_Numeral_Simprocs.less_cancel_numeral_factor\<close>
simproc_setup nat_le_cancel_numeral_factor
("(l::nat) * m <= n" | "(l::nat) <= m * n") =
- \<open>fn phi => Nat_Numeral_Simprocs.le_cancel_numeral_factor\<close>
+ \<open>K Nat_Numeral_Simprocs.le_cancel_numeral_factor\<close>
simproc_setup nat_div_cancel_numeral_factor
("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
- \<open>fn phi => Nat_Numeral_Simprocs.div_cancel_numeral_factor\<close>
+ \<open>K Nat_Numeral_Simprocs.div_cancel_numeral_factor\<close>
simproc_setup nat_dvd_cancel_numeral_factor
("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
- \<open>fn phi => Nat_Numeral_Simprocs.dvd_cancel_numeral_factor\<close>
+ \<open>K Nat_Numeral_Simprocs.dvd_cancel_numeral_factor\<close>
simproc_setup nat_eq_cancel_factor
("(l::nat) * m = n" | "(l::nat) = m * n") =
- \<open>fn phi => Nat_Numeral_Simprocs.eq_cancel_factor\<close>
+ \<open>K Nat_Numeral_Simprocs.eq_cancel_factor\<close>
simproc_setup nat_less_cancel_factor
("(l::nat) * m < n" | "(l::nat) < m * n") =
- \<open>fn phi => Nat_Numeral_Simprocs.less_cancel_factor\<close>
+ \<open>K Nat_Numeral_Simprocs.less_cancel_factor\<close>
simproc_setup nat_le_cancel_factor
("(l::nat) * m <= n" | "(l::nat) <= m * n") =
- \<open>fn phi => Nat_Numeral_Simprocs.le_cancel_factor\<close>
+ \<open>K Nat_Numeral_Simprocs.le_cancel_factor\<close>
simproc_setup nat_div_cancel_factor
("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
- \<open>fn phi => Nat_Numeral_Simprocs.div_cancel_factor\<close>
+ \<open>K Nat_Numeral_Simprocs.div_cancel_factor\<close>
simproc_setup nat_dvd_cancel_factor
("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
- \<open>fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor\<close>
+ \<open>K Nat_Numeral_Simprocs.dvd_cancel_factor\<close>
declaration \<open>
K (Lin_Arith.add_simprocs
--- a/src/HOL/Product_Type.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Product_Type.thy Thu May 25 13:58:46 2023 +0200
@@ -73,9 +73,9 @@
\<close>
simproc_setup unit_eq ("x::unit") = \<open>
- fn _ => fn _ => fn ct =>
+ K (K (fn ct =>
if HOLogic.is_unit (Thm.term_of ct) then NONE
- else SOME (mk_meta_eq @{thm unit_eq})
+ else SOME (mk_meta_eq @{thm unit_eq})))
\<close>
free_constructors case_unit for "()"
@@ -570,9 +570,9 @@
end;
\<close>
simproc_setup case_prod_beta ("case_prod f z") =
- \<open>fn _ => fn ctxt => fn ct => beta_proc ctxt (Thm.term_of ct)\<close>
+ \<open>K (fn ctxt => fn ct => beta_proc ctxt (Thm.term_of ct))\<close>
simproc_setup case_prod_eta ("case_prod f") =
- \<open>fn _ => fn ctxt => fn ct => eta_proc ctxt (Thm.term_of ct)\<close>
+ \<open>K (fn ctxt => fn ct => eta_proc ctxt (Thm.term_of ct))\<close>
lemma case_prod_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))"
by (auto simp: fun_eq_iff)
@@ -1326,7 +1326,7 @@
(* simplify {(x1, ..., xn). (x1, ..., xn) : S} to S *)
simproc_setup Collect_mem ("Collect t") = \<open>
- fn _ => fn ctxt => fn ct =>
+ K (fn ctxt => fn ct =>
(case Thm.term_of ct of
S as Const (\<^const_name>\<open>Collect\<close>, Type (\<^type_name>\<open>fun\<close>, [_, T])) $ t =>
let val (u, _, ps) = HOLogic.strip_ptupleabs t in
@@ -1355,7 +1355,7 @@
else NONE)
| _ => NONE)
end
- | _ => NONE)
+ | _ => NONE))
\<close>
ML_file \<open>Tools/inductive_set.ML\<close>
--- a/src/HOL/Real_Asymp/exp_log_expression.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Real_Asymp/exp_log_expression.ML Thu May 25 13:58:46 2023 +0200
@@ -229,7 +229,7 @@
fun decl phi =
register_custom' binding (Morphism.term phi pat) expand
in
- Local_Theory.declaration {syntax = false, pervasive = false} decl
+ Local_Theory.declaration {syntax = false, pervasive = false, pos = Binding.pos_of binding} decl
end
fun register_custom_from_thm binding thm expand =
--- a/src/HOL/Set.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Set.thy Thu May 25 13:58:46 2023 +0200
@@ -65,13 +65,13 @@
\<close>
simproc_setup defined_Collect ("{x. P x \<and> Q x}") = \<open>
- fn _ => Quantifier1.rearrange_Collect
+ K (Quantifier1.rearrange_Collect
(fn ctxt =>
resolve_tac ctxt @{thms Collect_cong} 1 THEN
resolve_tac ctxt @{thms iffI} 1 THEN
ALLGOALS
(EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms conjE},
- DEPTH_SOLVE_1 o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms conjI})]))
+ DEPTH_SOLVE_1 o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms conjI})])))
\<close>
lemmas CollectE = CollectD [elim_format]
@@ -330,13 +330,11 @@
\<close>
simproc_setup defined_Bex ("\<exists>x\<in>A. P x \<and> Q x") = \<open>
- fn _ => Quantifier1.rearrange_Bex
- (fn ctxt => unfold_tac ctxt @{thms Bex_def})
+ K (Quantifier1.rearrange_Bex (fn ctxt => unfold_tac ctxt @{thms Bex_def}))
\<close>
simproc_setup defined_All ("\<forall>x\<in>A. P x \<longrightarrow> Q x") = \<open>
- fn _ => Quantifier1.rearrange_Ball
- (fn ctxt => unfold_tac ctxt @{thms Ball_def})
+ K (Quantifier1.rearrange_Ball (fn ctxt => unfold_tac ctxt @{thms Ball_def}))
\<close>
lemma ballI [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> P x) \<Longrightarrow> \<forall>x\<in>A. P x"
--- a/src/HOL/Statespace/state_space.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Statespace/state_space.ML Thu May 25 13:58:46 2023 +0200
@@ -346,7 +346,7 @@
|> map_distinctthm (K tt');
in context' end));
- val attr = Attrib.internal type_attr;
+ val attr = Attrib.internal \<^here> type_attr;
val assume =
((Binding.name dist_thm_name, [attr]),
@@ -378,7 +378,9 @@
fun add_declaration name decl thy =
thy
|> Named_Target.init [] name
- |> (fn lthy => Local_Theory.declaration {syntax = true, pervasive = false} (decl lthy) lthy)
+ |> (fn lthy =>
+ Local_Theory.declaration {syntax = true, pervasive = false, pos = Position.thread_data ()}
+ (decl lthy) lthy)
|> Local_Theory.exit_global;
fun parent_components thy (Ts, pname, renaming) =
--- a/src/HOL/Tools/BNF/bnf_def.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML Thu May 25 13:58:46 2023 +0200
@@ -2081,7 +2081,7 @@
val interpret_bnf = BNF_Plugin.data;
fun register_bnf_raw key bnf =
- Local_Theory.declaration {syntax = false, pervasive = true}
+ Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
(fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf)));
fun register_bnf plugins key bnf =
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu May 25 13:58:46 2023 +0200
@@ -418,7 +418,7 @@
val register_fp_sugars_raw =
fold (fn fp_sugar as {T = Type (s, _), ...} =>
- Local_Theory.declaration {syntax = false, pervasive = true}
+ Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
(fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar))));
fun register_fp_sugars plugins fp_sugars =
@@ -1069,7 +1069,7 @@
|> rotate_prems ~1;
val cases_set_attr =
- Attrib.internal (K (Induct.cases_pred (name_of_set set)));
+ Attrib.internal \<^here> (K (Induct.cases_pred (name_of_set set)));
val ctr_names = quasi_unambiguous_case_names (flat
(map (uncurry mk_names o map_prod length name_of_ctr) (premss ~~ ctrAs)));
@@ -2031,7 +2031,7 @@
|> Thm.close_derivation \<^here>;
val case_names_attr = Attrib.case_names (quasi_unambiguous_case_names case_names);
- val induct_set_attrs = map (Attrib.internal o K o Induct.induct_pred o name_of_set) sets;
+ val induct_set_attrs = map (Attrib.internal \<^here> o K o Induct.induct_pred o name_of_set) sets;
in
(thm, case_names_attr :: induct_set_attrs)
end
@@ -2647,8 +2647,8 @@
val rec_transfer_thmss =
map single (derive_rec_transfer_thms lthy recs rec_defs recs_args_types);
- val induct_type_attr = Attrib.internal o K o Induct.induct_type;
- val induct_pred_attr = Attrib.internal o K o Induct.induct_pred;
+ val induct_type_attr = Attrib.internal \<^here> o K o Induct.induct_type;
+ val induct_pred_attr = Attrib.internal \<^here> o K o Induct.induct_pred;
val ((rel_induct_thmss, common_rel_induct_thms),
(rel_induct_attrs, common_rel_induct_attrs)) =
@@ -2808,8 +2808,8 @@
val corec_code_thms = map (eq_ifIN lthy) corec_thmss;
val corec_sel_thmss = map flat corec_sel_thmsss;
- val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
- val coinduct_pred_attr = Attrib.internal o K o Induct.coinduct_pred;
+ val coinduct_type_attr = Attrib.internal \<^here> o K o Induct.coinduct_type;
+ val coinduct_pred_attr = Attrib.internal \<^here> o K o Induct.coinduct_pred;
val flat_corec_thms = append oo append;
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu May 25 13:58:46 2023 +0200
@@ -59,7 +59,7 @@
#> Option.map (transfer_n2m_sugar (Proof_Context.theory_of ctxt));
fun register_n2m_sugar key n2m_sugar =
- Local_Theory.declaration {syntax = false, pervasive = false}
+ Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
(fn phi => Data.map (Typtab.update (key, morph_n2m_sugar phi n2m_sugar)));
fun unfold_lets_splits (Const (\<^const_name>\<open>Let\<close>, _) $ t $ u) =
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Thu May 25 13:58:46 2023 +0200
@@ -2909,7 +2909,7 @@
end;
fun set_corec_info_exprs fpT_name f =
- Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
+ Local_Theory.declaration {syntax = false, pervasive = true, pos = Position.thread_data ()} (fn phi =>
let val exprs = f phi in
Data.map (apsnd (fn [info_tab] => [Symtab.map_default (fpT_name, exprs) (K exprs) info_tab]))
end);
@@ -3214,7 +3214,7 @@
let
val (info_tab', lthy) = fold_rev (uncurry o merge_corec_info_tabs) info_tabs (info_tab, lthy);
in
- Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
+ Local_Theory.declaration {syntax = false, pervasive = true, pos = Position.thread_data ()} (fn phi =>
Data.map (apsnd (fn _ => [Symtab.map (K (map (morph_corec_info_expr phi))) info_tab'])))
lthy
end);
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Thu May 25 13:58:46 2023 +0200
@@ -143,8 +143,9 @@
);
fun register_codatatype_extra fpT_name extra =
- Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
- Data.map (@{apply 3(1)} (Symtab.update (fpT_name, morph_codatatype_extra phi extra))));
+ Local_Theory.declaration {syntax = false, pervasive = true, pos = Position.thread_data ()}
+ (fn phi =>
+ Data.map (@{apply 3(1)} (Symtab.update (fpT_name, morph_codatatype_extra phi extra))));
fun codatatype_extra_of ctxt =
Symtab.lookup (#1 (Data.get (Context.Proof ctxt)))
@@ -154,19 +155,21 @@
Symtab.dest (#1 (Data.get (Context.Proof ctxt)));
fun register_coinduct_extra fpT_name extra =
- Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
- Data.map (@{apply 3(2)} (Symtab.update (fpT_name, morph_coinduct_extra phi extra))));
+ Local_Theory.declaration {syntax = false, pervasive = true, pos = Position.thread_data ()}
+ (fn phi =>
+ Data.map (@{apply 3(2)} (Symtab.update (fpT_name, morph_coinduct_extra phi extra))));
fun coinduct_extra_of ctxt =
Symtab.lookup (#2 (Data.get (Context.Proof ctxt)))
#> Option.map (transfer_coinduct_extra (Proof_Context.theory_of ctxt));
fun register_friend_extra fun_name eq_algrho algrho_eq =
- Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
- Data.map (@{apply 3(3)} (Symtab.map_default (fun_name, empty_friend_extra)
- (fn {eq_algrhos, algrho_eqs} =>
- {eq_algrhos = Morphism.thm phi eq_algrho :: eq_algrhos,
- algrho_eqs = Morphism.thm phi algrho_eq :: algrho_eqs}))));
+ Local_Theory.declaration {syntax = false, pervasive = true, pos = Position.thread_data ()}
+ (fn phi =>
+ Data.map (@{apply 3(3)} (Symtab.map_default (fun_name, empty_friend_extra)
+ (fn {eq_algrhos, algrho_eqs} =>
+ {eq_algrhos = Morphism.thm phi eq_algrho :: eq_algrhos,
+ algrho_eqs = Morphism.thm phi algrho_eq :: algrho_eqs}))));
fun all_friend_extras_of ctxt =
Symtab.dest (#3 (Data.get (Context.Proof ctxt)));
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu May 25 13:58:46 2023 +0200
@@ -382,7 +382,7 @@
val phi0 = substitute_noted_thm noted;
in
lthy3
- |> Local_Theory.declaration {syntax = false, pervasive = true}
+ |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
(fn phi => Data.map (@{fold 3} (fn T_name => fn Const (size_name, _) =>
fn overloaded_size_def =>
let val morph = Morphism.thm (phi0 $> phi) in
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Thu May 25 13:58:46 2023 +0200
@@ -210,7 +210,7 @@
val interpret_ctr_sugar = Ctr_Sugar_Plugin.data;
fun register_ctr_sugar_raw (ctr_sugar as {T = Type (name, _), ...}) =
- Local_Theory.declaration {syntax = false, pervasive = true}
+ Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
(fn phi => fn context =>
let val pos = Position.thread_data ()
in Data.map (Symtab.update (name, (pos, morph_ctr_sugar phi ctr_sugar))) context end);
@@ -1072,8 +1072,8 @@
|> Thm.close_derivation \<^here>
end;
- val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
- val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name));
+ val exhaust_case_names_attr = Attrib.internal \<^here> (K (Rule_Cases.case_names exhaust_cases));
+ val cases_type_attr = Attrib.internal \<^here> (K (Induct.cases_type fcT_name));
val nontriv_disc_eq_thmss =
map (map (fn th => th RS @{thm eq_False[THEN iffD2]}
@@ -1119,12 +1119,12 @@
(AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms))
|> fold (uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational))
(filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss))
- |> Local_Theory.declaration {syntax = false, pervasive = true}
+ |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
(fn phi => Case_Translation.register
(Morphism.term phi casex) (map (Morphism.term phi) ctrs))
|> plugins code_plugin ?
(Code.declare_default_eqns (map (rpair true) (flat nontriv_disc_eq_thmss @ case_thms @ all_sel_thms))
- #> Local_Theory.declaration {syntax = false, pervasive = false}
+ #> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
(fn phi => Context.mapping
(add_ctr_code fcT_name (map (Morphism.typ phi) As)
(map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
--- a/src/HOL/Tools/Function/function.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Tools/Function/function.ML Thu May 25 13:58:46 2023 +0200
@@ -129,7 +129,7 @@
(K false) (map fst fixes)
in
(info,
- lthy2 |> Local_Theory.declaration {syntax = false, pervasive = false}
+ lthy2 |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
(fn phi => add_function_data (transform_function_data phi info)))
end
in
@@ -209,7 +209,7 @@
in
(info',
lthy2
- |> Local_Theory.declaration {syntax = false, pervasive = false}
+ |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
(fn phi => add_function_data (transform_function_data phi info'))
|> Spec_Rules.add Binding.empty Spec_Rules.equational_recdef fs tsimps)
end)
--- a/src/HOL/Tools/Lifting/lifting_def.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Thu May 25 13:58:46 2023 +0200
@@ -528,7 +528,7 @@
val register_code_eq_attribute = Thm.declaration_attribute
(fn thm => Context.mapping (register_encoded_code_eq thm) I)
- val register_code_eq_attrib = Attrib.internal (K register_code_eq_attribute)
+ val register_code_eq_attrib = Attrib.internal \<^here> (K register_code_eq_attribute)
in
@@ -547,7 +547,7 @@
which code equation is going to be used. This is going to be resolved at the
point when an interpretation of the locale is executed. *)
val lthy'' = lthy'
- |> Local_Theory.declaration {syntax = false, pervasive = true} (K (Data.put NONE))
+ |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>} (K (Data.put NONE))
in (code_eq, lthy'') end
else
(NONE_EQ, lthy)
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Thu May 25 13:58:46 2023 +0200
@@ -146,7 +146,7 @@
fun update_code_dt code_dt =
(snd o Local_Theory.begin_nested)
- #> Local_Theory.declaration {syntax = false, pervasive = true}
+ #> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
(fn phi => Data.map (Item_Net.update (morph_code_dt phi code_dt)))
#> Local_Theory.end_nested
@@ -346,7 +346,7 @@
|> update_rep_isom rep_isom (transfer_rules_of_lift_def rep_isom_lift_def |> hd)
(bundle_name_of_bundle_binding qty_isom_bundle phi context) pointer;
val lthy3 = lthy2
- |> Local_Theory.declaration {syntax = false, pervasive = true}
+ |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
(fn phi => fn context => Data.map (Item_Net.update (morph_code_dt phi (code_dt phi context))) context)
|> Local_Theory.end_nested
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Thu May 25 13:58:46 2023 +0200
@@ -248,7 +248,7 @@
([dummy_thm], [map Token.make_string0 ["Lifting.lifting_restore_internal", bundle_name]])
in
lthy
- |> Local_Theory.declaration {syntax = false, pervasive = true}
+ |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
(fn phi => Lifting_Info.init_restore_data bundle_name (phi_qinfo phi))
|> Bundle.bundle ((binding, [restore_lifting_att])) []
|> pair binding
@@ -272,7 +272,7 @@
val quotients = { quot_thm = quot_thm, pcr_info = pcr_info }
val qty_full_name = (fst o dest_Type) qty
fun quot_info phi = Lifting_Info.transform_quotient phi quotients
- val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute)
+ val reflexivity_rule_attr = Attrib.internal \<^here> (K Lifting_Info.add_reflexivity_rule_attribute)
val lthy3 =
case opt_reflp_thm of
SOME reflp_thm =>
@@ -283,7 +283,7 @@
| NONE => lthy2 |> define_abs_type quot_thm
in
lthy3
- |> Local_Theory.declaration {syntax = false, pervasive = true}
+ |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
(fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
|> lifting_bundle qty_full_name quotients
end
@@ -520,7 +520,7 @@
val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy0) quot_thm
(**)
val (rty, qty) = quot_thm_rty_qty quot_thm
- val induct_attr = Attrib.internal (K (Induct.induct_type (fst (dest_Type qty))))
+ val induct_attr = Attrib.internal \<^here> (K (Induct.induct_type (fst (dest_Type qty))))
val qty_full_name = (fst o dest_Type) qty
val qty_name = (Binding.name o Long_Name.base_name) qty_full_name
val qualify = Binding.qualify_name true qty_name
@@ -997,7 +997,7 @@
val quot_thm = #quot_thm qinfo
val transfer_rules = get_transfer_rules_to_delete qinfo lthy
in
- Local_Theory.declaration {syntax = false, pervasive = true}
+ Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
(K (fold (Transfer.transfer_raw_del) transfer_rules #> Lifting_Info.delete_quotients quot_thm))
lthy
end
@@ -1029,7 +1029,7 @@
in
case Lifting_Info.lookup_restore_data lthy pointer of
SOME refresh_data =>
- Local_Theory.declaration {syntax = false, pervasive = true}
+ Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
(fn phi => Lifting_Info.add_transfer_rules_in_restore_data pointer
(new_transfer_rules refresh_data lthy phi)) lthy
| NONE => error "The lifting bundle refers to non-existent restore data."
--- a/src/HOL/Tools/Quotient/quotient_def.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Thu May 25 13:58:46 2023 +0200
@@ -74,7 +74,7 @@
val rsp_thm_name = qualify lhs_name "rsp"
val lthy'' = lthy'
- |> Local_Theory.declaration {syntax = false, pervasive = true}
+ |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
(fn phi =>
(case qconst_data phi of
qcinfo as {qconst = Const (c, _), ...} =>
--- a/src/HOL/Tools/Quotient/quotient_type.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Thu May 25 13:58:46 2023 +0200
@@ -149,7 +149,7 @@
Quotient_Info.transform_abs_rep phi {abs = abs, rep = rep}
in
lthy
- |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
+ |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>} (fn phi =>
Quotient_Info.update_quotients (qty_full_name, quotients phi) #>
Quotient_Info.update_abs_rep (qty_full_name, abs_rep phi))
|> setup_lifting_package quot_thm equiv_thm opt_par_thm
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Thu May 25 13:58:46 2023 +0200
@@ -208,7 +208,7 @@
lthy
|> Local_Theory.notes notes
|> snd
- |> Local_Theory.declaration {syntax = false, pervasive = true}
+ |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
(fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data))
end
@@ -260,7 +260,7 @@
|> Transfer.update_pred_simps pred_injects
in
lthy
- |> Local_Theory.declaration {syntax = false, pervasive = true}
+ |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
(fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data))
end
--- a/src/HOL/Tools/functor.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Tools/functor.ML Thu May 25 13:58:46 2023 +0200
@@ -263,7 +263,7 @@
|> Local_Theory.note ((qualify identityN, []),
[prove_identity lthy id_thm])
|> snd
- |> Local_Theory.declaration {syntax = false, pervasive = false}
+ |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
(mapper_declaration comp_thm id_thm))
in
lthy
--- a/src/HOL/Tools/inductive.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Tools/inductive.ML Thu May 25 13:58:46 2023 +0200
@@ -1032,7 +1032,7 @@
[Attrib.case_names [rec_name],
Attrib.case_conclusion (rec_name, intr_names),
Attrib.consumes (1 - Thm.nprems_of raw_induct),
- Attrib.internal (K (Induct.coinduct_pred (hd cnames)))])
+ Attrib.internal \<^here> (K (Induct.coinduct_pred (hd cnames)))])
else if no_ind orelse length cnames > 1 then
(raw_induct, ind_case_names @ [Attrib.consumes (~ (Thm.nprems_of raw_induct))])
else
@@ -1055,7 +1055,7 @@
((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
((if forall (equal "") cases then [] else [Attrib.case_names cases]) @
[Attrib.consumes (1 - Thm.nprems_of elim), Attrib.constraints k,
- Attrib.internal (K (Induct.cases_pred name))] @ @{attributes [Pure.elim?]})),
+ Attrib.internal \<^here> (K (Induct.cases_pred name))] @ @{attributes [Pure.elim?]})),
[elim]) #>
apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
Local_Theory.note
@@ -1065,7 +1065,7 @@
val (eqs', lthy3) = lthy2 |>
fold_map (fn (name, eq) => Local_Theory.note
((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"),
- [Attrib.internal (K equation_add_permissive)]), [eq])
+ [Attrib.internal \<^here> (K equation_add_permissive)]), [eq])
#> apfst (hd o snd))
(if null eqs then [] else (cnames ~~ eqs))
val (inducts, lthy4) =
@@ -1077,7 +1077,7 @@
inducts |> map (fn (name, th) => ([th],
ind_case_names @
[Attrib.consumes (1 - Thm.nprems_of th),
- Attrib.internal (K (Induct.induct_pred name))])))] |>> snd o hd
+ Attrib.internal \<^here> (K (Induct.induct_pred name))])))] |>> snd o hd
end;
in (intrs', elims', eqs', induct', inducts, lthy4) end;
@@ -1144,7 +1144,7 @@
eqs = eqs'};
val lthy4 = lthy3
- |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi =>
+ |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>} (fn phi =>
let val result' = transform_result phi result;
in put_inductives ({names = cnames, coind = coind}, result') end);
in (result, lthy4) end;
--- a/src/HOL/Tools/inductive_set.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Tools/inductive_set.ML Thu May 25 13:58:46 2023 +0200
@@ -494,7 +494,7 @@
[def, @{thm mem_Collect_eq}, @{thm case_prod_conv}]) 1))
in
lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
- [Attrib.internal (K pred_set_conv_att)]),
+ [Attrib.internal \<^here> (K pred_set_conv_att)]),
[conv_thm]) |> snd
end) (preds ~~ cs ~~ cs_info ~~ defs) lthy2;
--- a/src/HOL/Tools/semiring_normalizer.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Tools/semiring_normalizer.ML Thu May 25 13:58:46 2023 +0200
@@ -173,7 +173,7 @@
val raw_ring = prepare_ops raw_ring0;
val raw_field = prepare_ops raw_field0;
in
- lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
+ lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>} (fn phi => fn context =>
let
val ctxt = Context.proof_of context;
val key = Morphism.thm phi raw_key;
--- a/src/HOL/Tools/typedef.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/HOL/Tools/typedef.ML Thu May 25 13:58:46 2023 +0200
@@ -259,19 +259,19 @@
make @{thm type_definition.Abs_inject})
||>> note ((Binding.suffix_name "_cases" Rep_name,
[Attrib.case_names [Binding.name_of Rep_name],
- Attrib.internal (K (Induct.cases_pred full_name))]),
+ Attrib.internal \<^here> (K (Induct.cases_pred full_name))]),
make @{thm type_definition.Rep_cases})
||>> note ((Binding.suffix_name "_cases" Abs_name,
[Attrib.case_names [Binding.name_of Abs_name],
- Attrib.internal (K (Induct.cases_type full_name))]),
+ Attrib.internal \<^here> (K (Induct.cases_type full_name))]),
make @{thm type_definition.Abs_cases})
||>> note ((Binding.suffix_name "_induct" Rep_name,
[Attrib.case_names [Binding.name_of Rep_name],
- Attrib.internal (K (Induct.induct_pred full_name))]),
+ Attrib.internal \<^here> (K (Induct.induct_pred full_name))]),
make @{thm type_definition.Rep_induct})
||>> note ((Binding.suffix_name "_induct" Abs_name,
[Attrib.case_names [Binding.name_of Abs_name],
- Attrib.internal (K (Induct.induct_type full_name))]),
+ Attrib.internal \<^here> (K (Induct.induct_type full_name))]),
make @{thm type_definition.Abs_induct});
val info =
@@ -283,7 +283,7 @@
Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct});
in
lthy3
- |> Local_Theory.declaration {syntax = false, pervasive = true}
+ |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
(fn phi => put_info full_name (transform_info phi info))
|> Typedef_Plugin.data Plugin_Name.default_filter full_name
|> pair (full_name, info)
--- a/src/Provers/order_tac.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/Provers/order_tac.ML Thu May 25 13:58:46 2023 +0200
@@ -368,15 +368,16 @@
)
fun declare (octxt as {kind = kind, raw_proc = raw_proc, ...}) lthy =
- lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
- let
- val ops = map (Morphism.term phi) (#ops octxt)
- val thms = map (fn (s, thm) => (s, Morphism.thm phi thm)) (#thms octxt)
- val conv_thms = map (fn (s, thm) => (s, Morphism.thm phi thm)) (#conv_thms octxt)
- val octxt' = {kind = kind, ops = ops, thms = thms, conv_thms = conv_thms}
- in
- context |> Data.map (Library.insert order_data_eq (octxt', raw_proc))
- end)
+ lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
+ (fn phi => fn context =>
+ let
+ val ops = map (Morphism.term phi) (#ops octxt)
+ val thms = map (fn (s, thm) => (s, Morphism.thm phi thm)) (#thms octxt)
+ val conv_thms = map (fn (s, thm) => (s, Morphism.thm phi thm)) (#conv_thms octxt)
+ val octxt' = {kind = kind, ops = ops, thms = thms, conv_thms = conv_thms}
+ in
+ context |> Data.map (Library.insert order_data_eq (octxt', raw_proc))
+ end)
fun declare_order {
ops = {eq = eq, le = le, lt = lt},
--- a/src/Pure/Admin/isabelle_cronjob.scala Tue May 23 12:31:23 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Thu May 25 13:58:46 2023 +0200
@@ -57,8 +57,9 @@
""" -a --include="*/" --include="plain_identify*" --exclude="*" """ +
Bash.string(backup + "/log/.") + " " + File.bash_path(main_dir) + "/log/.").check
- if (!Isabelle_Devel.cronjob_log.is_file)
+ if (!Isabelle_Devel.cronjob_log.is_file) {
Files.createSymbolicLink(Isabelle_Devel.cronjob_log.java_path, current_log.java_path)
+ }
})
val exit: Logger_Task =
@@ -292,7 +293,7 @@
Remote_Build("macOS 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a",
detect = Build_Log.Prop.build_start.toString + " < date '2017-03-03'")) :::
{
- for { (n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy5")) }
+ for ((n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy5")))
yield {
Remote_Build("AFP old", host = hosts.head, more_hosts = hosts.tail,
options = "-m32 -M1x2 -t AFP -P" + n +
--- a/src/Pure/Isar/attrib.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/Pure/Isar/attrib.ML Thu May 25 13:58:46 2023 +0200
@@ -48,8 +48,8 @@
local_theory -> local_theory
val attribute_setup: bstring * Position.T -> Input.source -> string ->
local_theory -> local_theory
- val internal: (morphism -> attribute) -> Token.src
- val internal_declaration: Morphism.declaration_entity -> thms
+ val internal: Position.T -> (morphism -> attribute) -> Token.src
+ val internal_declaration: Position.T -> Morphism.declaration_entity -> thms
val add_del: attribute -> attribute -> attribute context_parser
val thm: thm context_parser
val thms: thm list context_parser
@@ -251,13 +251,15 @@
"internal attribute");
val internal_name = make_name (Context.the_local_context ()) (Binding.name_of internal_binding);
-val internal_arg = Token.make_string0 "<attribute>";
-fun internal_source value = [internal_name, Token.assign (SOME value) internal_arg];
+fun internal_source name value = [internal_name, Token.assign (SOME value) (Token.make_string name)];
in
-fun internal arg = internal_source (Token.Attribute (Morphism.entity arg));
-fun internal_declaration arg = [([Drule.dummy_thm], [internal_source (Token.Declaration arg)])];
+fun internal pos arg =
+ internal_source ("internal", pos) (Token.Attribute (Morphism.entity arg));
+
+fun internal_declaration pos arg =
+ [([Drule.dummy_thm], [internal_source ("declaration", pos) (Token.Declaration arg)])];
end;
--- a/src/Pure/Isar/bundle.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/Pure/Isar/bundle.ML Thu May 25 13:58:46 2023 +0200
@@ -129,7 +129,7 @@
|> transform_bundle (Proof_Context.export_morphism ctxt' lthy)
|> trim_context_bundle;
in
- lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
+ lthy |> Local_Theory.declaration {syntax = false, pervasive = true, pos = Binding.pos_of binding}
(fn phi => fn context =>
let val psi = Morphism.set_trim_context'' context phi
in #2 (define_bundle (Morphism.binding psi binding, transform_bundle psi bundle) context) end)
@@ -181,9 +181,9 @@
|> Attrib.local_notes kind facts
end;
-fun bundle_declaration decl lthy =
+fun bundle_declaration pos decl lthy =
lthy
- |> (augment_target o Attrib.internal_declaration)
+ |> (augment_target o Attrib.internal_declaration pos)
(Morphism.transform (Local_Theory.standard_morphism_theory lthy) decl)
|> Generic_Target.standard_declaration (K true) decl;
@@ -198,10 +198,10 @@
{define = bad_operation,
notes = bundle_notes,
abbrev = bad_operation,
- declaration = K bundle_declaration,
+ declaration = fn {pos, ...} => bundle_declaration pos,
theory_registration = bad_operation,
locale_dependency = bad_operation,
- pretty = pretty binding}
+ pretty = pretty binding};
end;
--- a/src/Pure/Isar/code.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/Pure/Isar/code.ML Thu May 25 13:58:46 2023 +0200
@@ -1310,7 +1310,7 @@
(* abstract code declarations *)
fun code_declaration strictness lift_phi f x =
- Local_Theory.declaration {syntax = false, pervasive = false}
+ Local_Theory.declaration {syntax = false, pervasive = false, pos = Position.thread_data ()}
(fn phi => Context.mapping (f strictness (lift_phi phi x)) I);
--- a/src/Pure/Isar/entity.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/Pure/Isar/entity.ML Thu May 25 13:58:46 2023 +0200
@@ -35,12 +35,13 @@
(* local definition *)
fun alias {get_data, put_data} binding name =
- Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
- let
- val naming = Name_Space.naming_of context;
- val binding' = Morphism.binding phi binding;
- val data' = Name_Space.alias_table naming binding' name (get_data context);
- in put_data data' context end);
+ Local_Theory.declaration {syntax = false, pervasive = false, pos = Binding.pos_of binding}
+ (fn phi => fn context =>
+ let
+ val naming = Name_Space.naming_of context;
+ val binding' = Morphism.binding phi binding;
+ val data' = Name_Space.alias_table naming binding' name (get_data context);
+ in put_data data' context end);
fun transfer {get_data, put_data} ctxt =
let
--- a/src/Pure/Isar/expression.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/Pure/Isar/expression.ML Thu May 25 13:58:46 2023 +0200
@@ -794,7 +794,7 @@
fun defines_to_notes ctxt (Defines defs) =
Notes ("", map (fn (a, (def, _)) =>
(a, [([Assumption.assume ctxt (Thm.cterm_of ctxt def)],
- [Attrib.internal (K Locale.witness_add)])])) defs)
+ [Attrib.internal @{here} (K Locale.witness_add)])])) defs)
| defines_to_notes _ e = e;
val is_hyp = fn Assumes _ => true | Defines _ => true | _ => false;
@@ -846,7 +846,7 @@
if is_some asm then
[("", [((Binding.suffix_name ("_" ^ axiomsN) binding, []),
[([Assumption.assume pred_ctxt (Thm.cterm_of pred_ctxt (the asm))],
- [Attrib.internal (K Locale.witness_add)])])])]
+ [Attrib.internal @{here} (K Locale.witness_add)])])])]
else [];
val notes' =
--- a/src/Pure/Isar/generic_target.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML Thu May 25 13:58:46 2023 +0200
@@ -63,16 +63,16 @@
local_theory -> local_theory
val locale_target_abbrev: string -> Syntax.mode ->
(binding * mixfix) -> term -> term list * term list -> local_theory -> local_theory
- val locale_target_declaration: string -> bool -> Morphism.declaration_entity ->
- local_theory -> local_theory
+ val locale_target_declaration: string -> {syntax: bool, pos: Position.T} ->
+ Morphism.declaration_entity -> local_theory -> local_theory
val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
(binding * mixfix) * term -> local_theory -> local_theory
(*locale operations*)
val locale_abbrev: string -> Syntax.mode -> (binding * mixfix) * term ->
local_theory -> (term * term) * local_theory
- val locale_declaration: string -> {syntax: bool, pervasive: bool} -> Morphism.declaration_entity ->
- local_theory -> local_theory
+ val locale_declaration: string -> {syntax: bool, pervasive: bool, pos: Position.T} ->
+ Morphism.declaration_entity -> local_theory -> local_theory
val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
local_theory -> local_theory
val locale_dependency: string -> Locale.registration ->
@@ -443,20 +443,21 @@
Locale.add_facts locale kind (standard_facts lthy ctxt local_facts))) #>
standard_notes (fn (this, other) => other <> 0 andalso this <> other) kind local_facts;
-fun locale_target_declaration locale syntax decl lthy = lthy
+fun locale_target_declaration locale params decl lthy = lthy
|> Local_Theory.target (fn ctxt => ctxt |>
- Locale.add_declaration locale syntax
+ Locale.add_declaration locale params
(Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl));
fun locale_target_const locale phi_pred prmode ((b, mx), rhs) =
- locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs))
+ locale_target_declaration locale {syntax = true, pos = Binding.pos_of b}
+ (const_decl phi_pred prmode ((b, mx), rhs));
(** locale operations **)
-fun locale_declaration locale {syntax, pervasive} decl =
+fun locale_declaration locale {syntax, pervasive, pos} decl =
pervasive ? background_declaration decl
- #> locale_target_declaration locale syntax decl
+ #> locale_target_declaration locale {syntax = syntax, pos = pos} decl
#> standard_declaration (fn (_, other) => other <> 0) decl;
fun locale_const locale prmode ((b, mx), rhs) =
--- a/src/Pure/Isar/isar_cmd.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Thu May 25 13:58:46 2023 +0200
@@ -130,7 +130,8 @@
ML_Context.expression (Input.pos_of source)
(ML_Lex.read
("Theory.local_setup (Local_Theory.declaration {syntax = " ^
- Bool.toString syntax ^ ", pervasive = " ^ Bool.toString pervasive ^ "} (") @
+ Bool.toString syntax ^ ", pervasive = " ^ Bool.toString pervasive ^
+ ", pos = " ^ ML_Syntax.print_position (Position.thread_data ()) ^ "} (") @
ML_Lex.read_source source @ ML_Lex.read "))")
|> Context.proof_map;
--- a/src/Pure/Isar/local_theory.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/Pure/Isar/local_theory.ML Thu May 25 13:58:46 2023 +0200
@@ -55,7 +55,7 @@
(string * thm list) list * local_theory
val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
(term * term) * local_theory
- val declaration: {syntax: bool, pervasive: bool} -> Morphism.declaration ->
+ val declaration: {syntax: bool, pervasive: bool, pos: Position.T} -> Morphism.declaration ->
local_theory -> local_theory
val theory_registration: Locale.registration -> local_theory -> local_theory
val locale_dependency: Locale.registration -> local_theory -> local_theory
@@ -103,7 +103,7 @@
notes: string -> Attrib.fact list -> local_theory -> (string * thm list) list * local_theory,
abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
(term * term) * local_theory,
- declaration: {syntax: bool, pervasive: bool} -> Morphism.declaration_entity ->
+ declaration: {syntax: bool, pervasive: bool, pos: Position.T} -> Morphism.declaration_entity ->
local_theory -> local_theory,
theory_registration: Locale.registration -> local_theory -> local_theory,
locale_dependency: Locale.registration -> local_theory -> local_theory,
@@ -301,7 +301,7 @@
|-> (fn name =>
map_contexts (fn _ => fn ctxt =>
Proof_Context.transfer_facts (Proof_Context.theory_of ctxt) ctxt) #>
- declaration {syntax = false, pervasive = false} (fn phi =>
+ declaration {syntax = false, pervasive = false, pos = Binding.pos_of binding} (fn phi =>
let val binding' = Morphism.binding phi binding in
Context.mapping
(Global_Theory.alias_fact binding' name)
@@ -312,7 +312,7 @@
(* default sort *)
fun set_defsort S =
- declaration {syntax = true, pervasive = false}
+ declaration {syntax = true, pervasive = false, pos = Position.thread_data ()}
(K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
@@ -324,7 +324,7 @@
val args' = map (fn (c, T, mx) => (c, T, Mixfix.reset_pos mx)) args;
val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.syntax add mode args;
in
- declaration {syntax = true, pervasive = false}
+ declaration {syntax = true, pervasive = false, pos = Position.thread_data ()}
(fn _ => Proof_Context.generic_syntax add mode args') lthy
end;
@@ -343,7 +343,7 @@
val args' = map (apsnd Mixfix.reset_pos) args;
val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.type_notation add mode args;
in
- declaration {syntax = true, pervasive = false}
+ declaration {syntax = true, pervasive = false, pos = Position.thread_data ()}
(Proof_Context.generic_type_notation add mode args') lthy
end;
@@ -354,7 +354,7 @@
val args' = map (apsnd Mixfix.reset_pos) args;
val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.notation add mode args;
in
- declaration {syntax = true, pervasive = false}
+ declaration {syntax = true, pervasive = false, pos = Position.thread_data ()}
(Proof_Context.generic_notation add mode args') lthy
end;
@@ -373,7 +373,7 @@
(* name space aliases *)
fun syntax_alias global_alias local_alias b name =
- declaration {syntax = true, pervasive = false} (fn phi =>
+ declaration {syntax = true, pervasive = false, pos = Position.thread_data ()} (fn phi =>
let val b' = Morphism.binding phi b
in Context.mapping (global_alias b' name) (local_alias b' name) end);
--- a/src/Pure/Isar/locale.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/Pure/Isar/locale.ML Thu May 25 13:58:46 2023 +0200
@@ -59,7 +59,8 @@
(* Storing results *)
val add_facts: string -> string -> Attrib.fact list -> Proof.context -> Proof.context
- val add_declaration: string -> bool -> Morphism.declaration_entity -> Proof.context -> Proof.context
+ val add_declaration: string -> {syntax: bool, pos: Position.T} ->
+ Morphism.declaration_entity -> Proof.context -> Proof.context
(* Activation *)
val activate_facts: morphism option -> string * morphism -> Context.generic -> Context.generic
@@ -674,11 +675,11 @@
((change_locale loc o apfst o apsnd) (cons stored_notes) #> apply_registrations)
end;
-fun add_declaration loc syntax decl =
+fun add_declaration loc {syntax, pos} decl =
let val decl0 = Morphism.entity_reset_context decl in
syntax ?
Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl0, serial ())))
- #> add_facts loc "" [(Binding.empty_atts, Attrib.internal_declaration decl0)]
+ #> add_facts loc "" [(Binding.empty_atts, Attrib.internal_declaration pos decl0)]
end;
--- a/src/Pure/Isar/method.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/Pure/Isar/method.ML Thu May 25 13:58:46 2023 +0200
@@ -608,7 +608,8 @@
val facts =
Attrib.partial_evaluation ctxt [((Binding.name "dummy", []), thms)]
|> map (fn (_, bs) =>
- ((Binding.empty, [Attrib.internal (K attribute)]), Attrib.trim_context_thms bs));
+ ((Binding.empty, [Attrib.internal pos (K attribute)]),
+ Attrib.trim_context_thms bs));
val decl =
Morphism.entity (fn phi => fn context =>
--- a/src/Pure/Isar/spec_rules.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/Pure/Isar/spec_rules.ML Thu May 25 13:58:46 2023 +0200
@@ -162,7 +162,7 @@
val n = length terms;
val thms0 = map Thm.trim_context (map (Drule.mk_term o Thm.cterm_of lthy) terms @ rules);
in
- lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
+ lthy |> Local_Theory.declaration {syntax = false, pervasive = true, pos = Binding.pos_of b}
(fn phi => fn context =>
let
val psi = Morphism.set_trim_context'' context phi;
--- a/src/Pure/Isar/token.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/Pure/Isar/token.ML Thu May 25 13:58:46 2023 +0200
@@ -558,6 +558,10 @@
(* pretty *)
+fun pretty_keyword3 tok =
+ let val props = Position.properties_of (pos_of tok)
+ in Pretty.mark_str (Markup.properties props Markup.keyword3, unparse tok) end;
+
fun pretty_value ctxt tok =
(case get_value tok of
SOME (Literal markup) =>
@@ -568,6 +572,8 @@
| SOME (Term t) => Syntax.pretty_term ctxt t
| SOME (Fact (_, ths)) =>
Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.cartouche o Thm.pretty_thm ctxt) ths))
+ | SOME (Attribute _) => pretty_keyword3 tok
+ | SOME (Declaration _) => pretty_keyword3 tok
| _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok));
--- a/src/Pure/ex/Def.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/Pure/ex/Def.thy Thu May 25 13:58:46 2023 +0200
@@ -41,7 +41,7 @@
fun declare_def lhs eq lthy =
let val def0: def = {lhs = lhs, eq = Thm.trim_context eq} in
- lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
+ lthy |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
(fn phi => fn context =>
let val psi = Morphism.set_trim_context'' context phi
in (Data.map o Item_Net.update) (transform_def psi def0) context end)
--- a/src/Pure/simplifier.ML Tue May 23 12:31:23 2023 +0100
+++ b/src/Pure/simplifier.ML Thu May 25 13:58:46 2023 +0200
@@ -139,15 +139,16 @@
val simproc =
make_simproc lthy (Local_Theory.full_name lthy b) {lhss = prep lthy lhss, proc = proc};
in
- lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
- let
- val b' = Morphism.binding phi b;
- val simproc' = transform_simproc phi simproc;
- in
- context
- |> Simprocs.map (#2 o Name_Space.define context true (b', simproc'))
- |> map_ss (fn ctxt => ctxt addsimprocs [simproc'])
- end)
+ lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = Binding.pos_of b}
+ (fn phi => fn context =>
+ let
+ val b' = Morphism.binding phi b;
+ val simproc' = transform_simproc phi simproc;
+ in
+ context
+ |> Simprocs.map (#2 o Name_Space.define context true (b', simproc'))
+ |> map_ss (fn ctxt => ctxt addsimprocs [simproc'])
+ end)
end;
in
--- a/src/ZF/OrdQuant.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/ZF/OrdQuant.thy Thu May 25 13:58:46 2023 +0200
@@ -350,13 +350,11 @@
text \<open>Setting up the one-point-rule simproc\<close>
simproc_setup defined_rex ("\<exists>x[M]. P(x) \<and> Q(x)") = \<open>
- fn _ => Quantifier1.rearrange_Bex
- (fn ctxt => unfold_tac ctxt @{thms rex_def})
+ K (Quantifier1.rearrange_Bex (fn ctxt => unfold_tac ctxt @{thms rex_def}))
\<close>
simproc_setup defined_rall ("\<forall>x[M]. P(x) \<longrightarrow> Q(x)") = \<open>
- fn _ => Quantifier1.rearrange_Ball
- (fn ctxt => unfold_tac ctxt @{thms rall_def})
+ K (Quantifier1.rearrange_Ball (fn ctxt => unfold_tac ctxt @{thms rall_def}))
\<close>
end
--- a/src/ZF/pair.thy Tue May 23 12:31:23 2023 +0100
+++ b/src/ZF/pair.thy Thu May 25 13:58:46 2023 +0200
@@ -19,13 +19,11 @@
ML \<open>val ZF_ss = simpset_of \<^context>\<close>
simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) \<and> Q(x)") = \<open>
- fn _ => Quantifier1.rearrange_Bex
- (fn ctxt => unfold_tac ctxt @{thms Bex_def})
+ K (Quantifier1.rearrange_Bex (fn ctxt => unfold_tac ctxt @{thms Bex_def}))
\<close>
simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = \<open>
- fn _ => Quantifier1.rearrange_Ball
- (fn ctxt => unfold_tac ctxt @{thms Ball_def})
+ K (Quantifier1.rearrange_Ball (fn ctxt => unfold_tac ctxt @{thms Ball_def}))
\<close>