# HG changeset patch # User wenzelm # Date 1685015926 -7200 # Node ID 300537844bb7ddf1a63db47f5426198bf9cb7d60 # Parent cec875dcc59ee05faf2316508d03b2e3729f2425# Parent 35439ca0133c62013cb3f91fb44fd4f9780e3eb4 merged diff -r cec875dcc59e -r 300537844bb7 src/Doc/Isar_Ref/Generic.thy --- 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") = - \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})))\ (*<*)end(*>*) text \ diff -r cec875dcc59e -r 300537844bb7 src/HOL/Bali/Eval.thy --- 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\s \In1l t\\ (w, s')") = \ - fn _ => fn _ => fn ct => + K (K (fn ct => (case Thm.term_of ct of (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE - | _ => SOME (mk_meta_eq @{thm eval_expr_eq}))\ + | _ => SOME (mk_meta_eq @{thm eval_expr_eq}))))\ simproc_setup eval_var ("G\s \In2 t\\ (w, s')") = \ - fn _ => fn _ => fn ct => + K (K (fn ct => (case Thm.term_of ct of (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE - | _ => SOME (mk_meta_eq @{thm eval_var_eq}))\ + | _ => SOME (mk_meta_eq @{thm eval_var_eq}))))\ simproc_setup eval_exprs ("G\s \In3 t\\ (w, s')") = \ - fn _ => fn _ => fn ct => + K (K (fn ct => (case Thm.term_of ct of (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE - | _ => SOME (mk_meta_eq @{thm eval_exprs_eq}))\ + | _ => SOME (mk_meta_eq @{thm eval_exprs_eq}))))\ simproc_setup eval_stmt ("G\s \In1r t\\ (w, s')") = \ - fn _ => fn _ => fn ct => + K (K (fn ct => (case Thm.term_of ct of (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE - | _ => SOME (mk_meta_eq @{thm eval_stmt_eq}))\ + | _ => SOME (mk_meta_eq @{thm eval_stmt_eq}))))\ ML \ ML_Thms.bind_thms ("AbruptIs", sum3_instantiate \<^context> @{thm eval.Abrupt}) @@ -947,10 +947,10 @@ done simproc_setup eval_no_abrupt ("G\(x,s) \e\\ (w,Norm s')") = \ - fn _ => fn _ => fn ct => + K (K (fn ct => (case Thm.term_of ct of (_ $ _ $ (Const (\<^const_name>\Pair\, _) $ (Const (\<^const_name>\None\, _)) $ _) $ _ $ _ $ _) => NONE - | _ => SOME (mk_meta_eq @{thm eval_no_abrupt})) + | _ => SOME (mk_meta_eq @{thm eval_no_abrupt})))) \ @@ -967,10 +967,10 @@ done simproc_setup eval_abrupt ("G\(Some xc,s) \e\\ (w,s')") = \ - fn _ => fn _ => fn ct => + K (K (fn ct => (case Thm.term_of ct of (_ $ _ $ _ $ _ $ _ $ (Const (\<^const_name>\Pair\, _) $ (Const (\<^const_name>\Some\, _) $ _)$ _)) => NONE - | _ => SOME (mk_meta_eq @{thm eval_abrupt})) + | _ => SOME (mk_meta_eq @{thm eval_abrupt})))) \ lemma LitI: "G\s \Lit v-\(if normal s then v else undefined)\ s" diff -r cec875dcc59e -r 300537844bb7 src/HOL/Bali/Evaln.thy --- 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\s \In1l t\\n\ (w, s')") = \ - fn _ => fn _ => fn ct => + K (K (fn ct => (case Thm.term_of ct of (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE - | _ => SOME (mk_meta_eq @{thm evaln_expr_eq}))\ + | _ => SOME (mk_meta_eq @{thm evaln_expr_eq}))))\ simproc_setup evaln_var ("G\s \In2 t\\n\ (w, s')") = \ - fn _ => fn _ => fn ct => + K (K (fn ct => (case Thm.term_of ct of (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE - | _ => SOME (mk_meta_eq @{thm evaln_var_eq}))\ + | _ => SOME (mk_meta_eq @{thm evaln_var_eq}))))\ simproc_setup evaln_exprs ("G\s \In3 t\\n\ (w, s')") = \ - fn _ => fn _ => fn ct => + K (K (fn ct => (case Thm.term_of ct of (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE - | _ => SOME (mk_meta_eq @{thm evaln_exprs_eq}))\ + | _ => SOME (mk_meta_eq @{thm evaln_exprs_eq}))))\ simproc_setup evaln_stmt ("G\s \In1r t\\n\ (w, s')") = \ - fn _ => fn _ => fn ct => + K (K (fn ct => (case Thm.term_of ct of (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE - | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq}))\ + | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq}))))\ ML \ML_Thms.bind_thms ("evaln_AbruptIs", sum3_instantiate \<^context> @{thm evaln.Abrupt})\ declare evaln_AbruptIs [intro!] @@ -356,11 +356,11 @@ done simproc_setup evaln_abrupt ("G\(Some xc,s) \e\\n\ (w,s')") = \ - fn _ => fn _ => fn ct => + K (K (fn ct => (case Thm.term_of ct of (_ $ _ $ _ $ _ $ _ $ _ $ (Const (\<^const_name>\Pair\, _) $ (Const (\<^const_name>\Some\,_) $ _)$ _)) => NONE - | _ => SOME (mk_meta_eq @{thm evaln_abrupt})) + | _ => SOME (mk_meta_eq @{thm evaln_abrupt})))) \ lemma evaln_LitI: "G\s \Lit v-\(if normal s then v else undefined)\n\ s" diff -r cec875dcc59e -r 300537844bb7 src/HOL/Bali/WellType.thy --- 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\In1l t\U") = \ - fn _ => fn _ => fn ct => + K (K (fn ct => (case Thm.term_of ct of (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE - | _ => SOME (mk_meta_eq @{thm wt_expr_eq}))\ + | _ => SOME (mk_meta_eq @{thm wt_expr_eq}))))\ simproc_setup wt_var ("E,dt\In2 t\U") = \ - fn _ => fn _ => fn ct => + K (K (fn ct => (case Thm.term_of ct of (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE - | _ => SOME (mk_meta_eq @{thm wt_var_eq}))\ + | _ => SOME (mk_meta_eq @{thm wt_var_eq}))))\ simproc_setup wt_exprs ("E,dt\In3 t\U") = \ - fn _ => fn _ => fn ct => + K (K (fn ct => (case Thm.term_of ct of (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE - | _ => SOME (mk_meta_eq @{thm wt_exprs_eq}))\ + | _ => SOME (mk_meta_eq @{thm wt_exprs_eq}))))\ simproc_setup wt_stmt ("E,dt\In1r t\U") = \ - fn _ => fn _ => fn ct => + K (K (fn ct => (case Thm.term_of ct of (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE - | _ => SOME (mk_meta_eq @{thm wt_stmt_eq}))\ + | _ => SOME (mk_meta_eq @{thm wt_stmt_eq}))))\ lemma wt_elim_BinOp: "\E,dt\In1l (BinOp binop e1 e2)\T; diff -r cec875dcc59e -r 300537844bb7 src/HOL/Boolean_Algebras.thy --- 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 \Tools/boolean_algebra_cancel.ML\ simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") = - \fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_sup_conv\ + \K (K (try Boolean_Algebra_Cancel.cancel_sup_conv))\ simproc_setup boolean_algebra_cancel_inf ("inf a b::'a::boolean_algebra") = - \fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_inf_conv\ + \K (K (try Boolean_Algebra_Cancel.cancel_inf_conv))\ context boolean_algebra diff -r cec875dcc59e -r 300537844bb7 src/HOL/Data_Structures/Less_False.thy --- 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") = \fn _ => fn ctxt => fn ct => +simproc_setup less_False ("(x::'a::order) < y") = \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) \ end diff -r cec875dcc59e -r 300537844bb7 src/HOL/Decision_Procs/Commutative_Ring.thy --- 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 \ -Local_Theory.declaration {syntax = false, pervasive = false} - (fn phi => Ring_Tac.Ring_Simps.map (Ring_Tac.insert_rules Ring_Tac.eq_ring_simps +declaration \fn phi => + Ring_Tac.Ring_Simps.map (Ring_Tac.insert_rules Ring_Tac.eq_ring_simps (Morphism.term phi \<^term>\R\, (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]}))) \ end diff -r cec875dcc59e -r 300537844bb7 src/HOL/Decision_Procs/Conversions.thy --- 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 @@ \ attribute_setup meta = - \Scan.succeed (fn (ctxt, th) => (NONE, SOME (mk_meta_eq th)))\ + \Scan.succeed (Thm.rule_attribute [] (K mk_meta_eq))\ \convert equality to meta equality\ ML \ diff -r cec875dcc59e -r 300537844bb7 src/HOL/Decision_Procs/Reflective_Field.thy --- 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 \ -Local_Theory.declaration {syntax = false, pervasive = false} - (fn phi => Field_Tac.Field_Simps.map (Ring_Tac.insert_rules Field_Tac.eq_field_simps +declaration \fn phi => + Field_Tac.Field_Simps.map (Ring_Tac.insert_rules Field_Tac.eq_field_simps (Morphism.term phi \<^term>\R\, (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}))) \ end diff -r cec875dcc59e -r 300537844bb7 src/HOL/Eisbach/Tests.thy --- 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 - \Local_Theory.declaration {pervasive = false, syntax = false} - (fn phi => Data.put (Morphism.fact phi @{thms A}))\ +declaration \fn phi => Data.put (Morphism.fact phi @{thms A})\ lemma A by dynamic_thms_test diff -r cec875dcc59e -r 300537844bb7 src/HOL/Eisbach/method_closure.ML --- 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; diff -r cec875dcc59e -r 300537844bb7 src/HOL/Enum.thy --- 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") = \ - fn _ => fn _ => fn ct => + K (K (fn ct => (case Thm.term_of ct of Const (\<^const_name>\a\<^sub>1\, _) => NONE - | _ => SOME (mk_meta_eq @{thm finite_1_eq})) + | _ => SOME (mk_meta_eq @{thm finite_1_eq})))) \ instantiation finite_1 :: complete_boolean_algebra diff -r cec875dcc59e -r 300537844bb7 src/HOL/Finite_Set.thy --- 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 \ B \ finite B \ finite A" by (rule rev_finite_subset) -simproc_setup finite ("finite A") = \fn _ => +simproc_setup finite ("finite A") = \ 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 \ (* Needs to be used with care *) diff -r cec875dcc59e -r 300537844bb7 src/HOL/Fun.thy --- 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 \Simplify terms of the form \f(\,x:=y,\,x:=z,\)\ to \f(\,x:=z,\)\\ -simproc_setup fun_upd2 ("f(v := w, x := y)") = \fn _ => +simproc_setup fun_upd2 ("f(v := w, x := y)") = \ let fun gen_fun_upd NONE T _ _ = NONE | gen_fun_upd (SOME f) T x y = SOME (Const (\<^const_name>\fun_upd\, 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 \ diff -r cec875dcc59e -r 300537844bb7 src/HOL/Groups.thy --- 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) \ -simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc -simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc +simproc_setup reorient_zero ("0 = x") = \K Reorient_Proc.proc\ +simproc_setup reorient_one ("1 = x") = \K Reorient_Proc.proc\ typed_print_translation \ let diff -r cec875dcc59e -r 300537844bb7 src/HOL/HOL.thy --- 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 \Simproc for proving \(y = x) \ False\ from premise \\ (x = y)\:\ -simproc_setup neq ("x = y") = \fn _ => +simproc_setup neq ("x = y") = \ 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 \ simproc_setup let_simp ("Let x f") = \ @@ -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 \ @@ -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") = \fn _ => fn ctxt => fn ct => +simproc_setup NO_MATCH ("NO_MATCH pat val") = \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) \ text \ diff -r cec875dcc59e -r 300537844bb7 src/HOL/HOLCF/Cfun.thy --- 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 @@ \ simproc_setup beta_cfun_proc ("Rep_cfun (Abs_cfun f)") = \ - 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>\cont2cont\; 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) \ text \Eta-equality for continuous functions\ diff -r cec875dcc59e -r 300537844bb7 src/HOL/HOLCF/Pcpo.thy --- 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 \Simproc to rewrite \<^term>\\ = x\ to \<^term>\x = \\.\ setup \Reorient_Proc.add (fn \<^Const_>\bottom _\ => true | _ => false)\ -simproc_setup reorient_bottom ("\ = x") = Reorient_Proc.proc +simproc_setup reorient_bottom ("\ = x") = \K Reorient_Proc.proc\ text \useful lemmas about \<^term>\\\\ diff -r cec875dcc59e -r 300537844bb7 src/HOL/HOLCF/Tools/fixrec.ML --- 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 diff -r cec875dcc59e -r 300537844bb7 src/HOL/Library/Extended_Nat.thy --- 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") = - \fn phi => fn ctxt => fn ct => Eq_Enat_Cancel.proc ctxt (Thm.term_of ct)\ + \K (fn ctxt => fn ct => Eq_Enat_Cancel.proc ctxt (Thm.term_of ct))\ simproc_setup enat_le_cancel ("(l::enat) + m \ n" | "(l::enat) \ m + n") = - \fn phi => fn ctxt => fn ct => Le_Enat_Cancel.proc ctxt (Thm.term_of ct)\ + \K (fn ctxt => fn ct => Le_Enat_Cancel.proc ctxt (Thm.term_of ct))\ simproc_setup enat_less_cancel ("(l::enat) + m < n" | "(l::enat) < m + n") = - \fn phi => fn ctxt => fn ct => Less_Enat_Cancel.proc ctxt (Thm.term_of ct)\ + \K (fn ctxt => fn ct => Less_Enat_Cancel.proc ctxt (Thm.term_of ct))\ text \TODO: add regression tests for these simprocs\ diff -r cec875dcc59e -r 300537844bb7 src/HOL/Library/Extended_Nonnegative_Real.thy --- 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") = - \fn phi => fn ctxt => fn ct => Eq_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\ + \K (fn ctxt => fn ct => Eq_Ennreal_Cancel.proc ctxt (Thm.term_of ct))\ simproc_setup ennreal_le_cancel ("(l::ennreal) + m \ n" | "(l::ennreal) \ m + n") = - \fn phi => fn ctxt => fn ct => Le_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\ + \K (fn ctxt => fn ct => Le_Ennreal_Cancel.proc ctxt (Thm.term_of ct))\ simproc_setup ennreal_less_cancel ("(l::ennreal) + m < n" | "(l::ennreal) < m + n") = - \fn phi => fn ctxt => fn ct => Less_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\ + \K (fn ctxt => fn ct => Less_Ennreal_Cancel.proc ctxt (Thm.term_of ct))\ subsection \Order with top\ diff -r cec875dcc59e -r 300537844bb7 src/HOL/Library/Multiset.thy --- 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") = - \fn phi => Cancel_Simprocs.eq_cancel\ + \K Cancel_Simprocs.eq_cancel\ simproc_setup msetsubset_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") = - \fn phi => Multiset_Simprocs.subset_cancel_msets\ + \K Multiset_Simprocs.subset_cancel_msets\ simproc_setup msetsubset_eq_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") = - \fn phi => Multiset_Simprocs.subseteq_cancel_msets\ + \K Multiset_Simprocs.subseteq_cancel_msets\ 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") = - \fn phi => Cancel_Simprocs.diff_cancel\ + \K Cancel_Simprocs.diff_cancel\ subsubsection \Conditionally complete lattice\ diff -r cec875dcc59e -r 300537844bb7 src/HOL/Library/Multiset_Order.thy --- 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") = - \fn phi => Cancel_Simprocs.less_cancel\ + \K Cancel_Simprocs.less_cancel\ simproc_setup msetle_cancel ("(l::'a::preorder multiset) + m \ n" | "(l::'a multiset) \ m + n" | "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") = - \fn phi => Cancel_Simprocs.less_eq_cancel\ + \K Cancel_Simprocs.less_eq_cancel\ subsection \Additional facts and instantiations\ diff -r cec875dcc59e -r 300537844bb7 src/HOL/Library/adhoc_overloading.ML --- 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; diff -r cec875dcc59e -r 300537844bb7 src/HOL/List.thy --- 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 \ diff -r cec875dcc59e -r 300537844bb7 src/HOL/Nat.thy --- 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") = - \fn phi => try o Nat_Arith.cancel_eq_conv\ + \K (try o Nat_Arith.cancel_eq_conv)\ simproc_setup natless_cancel_sums ("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") = - \fn phi => try o Nat_Arith.cancel_less_conv\ + \K (try o Nat_Arith.cancel_less_conv)\ simproc_setup natle_cancel_sums ("(l::nat) + m \ n" | "(l::nat) \ m + n" | "Suc m \ n" | "m \ Suc n") = - \fn phi => try o Nat_Arith.cancel_le_conv\ + \K (try o Nat_Arith.cancel_le_conv)\ simproc_setup natdiff_cancel_sums ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") = - \fn phi => try o Nat_Arith.cancel_diff_conv\ + \K (try o Nat_Arith.cancel_diff_conv)\ context order begin diff -r cec875dcc59e -r 300537844bb7 src/HOL/Nominal/nominal_inductive.ML --- 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; diff -r cec875dcc59e -r 300537844bb7 src/HOL/Nominal/nominal_inductive2.ML --- 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; diff -r cec875dcc59e -r 300537844bb7 src/HOL/Nonstandard_Analysis/NSA.thy --- 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 \ x" | "1 \ y" | "numeral w \ z" | "- 1 \ y" | "- numeral w \ r") = \ 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 \ lemma Infinitesimal_approx_minus: "x - y \ Infinitesimal \ x \ y" diff -r cec875dcc59e -r 300537844bb7 src/HOL/Num.thy --- 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 @@ \ simproc_setup reorient_numeral ("numeral w = x" | "- numeral w = y") = - Reorient_Proc.proc + \K Reorient_Proc.proc\ subsubsection \Simplification of arithmetic operations on integer constants\ diff -r cec875dcc59e -r 300537844bb7 src/HOL/Numeral_Simprocs.thy --- 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") = - \fn phi => Numeral_Simprocs.assoc_fold\ + \K Numeral_Simprocs.assoc_fold\ (* 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") = - \fn phi => Numeral_Simprocs.combine_numerals\ + \K Numeral_Simprocs.combine_numerals\ simproc_setup field_combine_numerals ("(i::'a::{field,ring_char_0}) + j" |"(i::'a::{field,ring_char_0}) - j") = - \fn phi => Numeral_Simprocs.field_combine_numerals\ + \K Numeral_Simprocs.field_combine_numerals\ 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") = - \fn phi => Numeral_Simprocs.eq_cancel_numerals\ + \K Numeral_Simprocs.eq_cancel_numerals\ 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") = - \fn phi => Numeral_Simprocs.less_cancel_numerals\ + \K Numeral_Simprocs.less_cancel_numerals\ simproc_setup intle_cancel_numerals ("(l::'a::linordered_idom) + m \ n" @@ -147,138 +147,138 @@ |"(l::'a::linordered_idom) \ m * n" |"- (l::'a::linordered_idom) \ m" |"(l::'a::linordered_idom) \ - m") = - \fn phi => Numeral_Simprocs.le_cancel_numerals\ + \K Numeral_Simprocs.le_cancel_numerals\ simproc_setup ring_eq_cancel_numeral_factor ("(l::'a::{idom,ring_char_0}) * m = n" |"(l::'a::{idom,ring_char_0}) = m * n") = - \fn phi => Numeral_Simprocs.eq_cancel_numeral_factor\ + \K Numeral_Simprocs.eq_cancel_numeral_factor\ simproc_setup ring_less_cancel_numeral_factor ("(l::'a::linordered_idom) * m < n" |"(l::'a::linordered_idom) < m * n") = - \fn phi => Numeral_Simprocs.less_cancel_numeral_factor\ + \K Numeral_Simprocs.less_cancel_numeral_factor\ simproc_setup ring_le_cancel_numeral_factor ("(l::'a::linordered_idom) * m <= n" |"(l::'a::linordered_idom) <= m * n") = - \fn phi => Numeral_Simprocs.le_cancel_numeral_factor\ + \K Numeral_Simprocs.le_cancel_numeral_factor\ (* 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)") = - \fn phi => Numeral_Simprocs.div_cancel_numeral_factor\ + \K Numeral_Simprocs.div_cancel_numeral_factor\ 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)") = - \fn phi => Numeral_Simprocs.divide_cancel_numeral_factor\ + \K Numeral_Simprocs.divide_cancel_numeral_factor\ simproc_setup ring_eq_cancel_factor ("(l::'a::idom) * m = n" | "(l::'a::idom) = m * n") = - \fn phi => Numeral_Simprocs.eq_cancel_factor\ + \K Numeral_Simprocs.eq_cancel_factor\ simproc_setup linordered_ring_le_cancel_factor ("(l::'a::linordered_idom) * m <= n" |"(l::'a::linordered_idom) <= m * n") = - \fn phi => Numeral_Simprocs.le_cancel_factor\ + \K Numeral_Simprocs.le_cancel_factor\ simproc_setup linordered_ring_less_cancel_factor ("(l::'a::linordered_idom) * m < n" |"(l::'a::linordered_idom) < m * n") = - \fn phi => Numeral_Simprocs.less_cancel_factor\ + \K Numeral_Simprocs.less_cancel_factor\ simproc_setup int_div_cancel_factor ("((l::'a::euclidean_semiring_cancel) * m) div n" |"(l::'a::euclidean_semiring_cancel) div (m * n)") = - \fn phi => Numeral_Simprocs.div_cancel_factor\ + \K Numeral_Simprocs.div_cancel_factor\ simproc_setup int_mod_cancel_factor ("((l::'a::euclidean_semiring_cancel) * m) mod n" |"(l::'a::euclidean_semiring_cancel) mod (m * n)") = - \fn phi => Numeral_Simprocs.mod_cancel_factor\ + \K Numeral_Simprocs.mod_cancel_factor\ simproc_setup dvd_cancel_factor ("((l::'a::idom) * m) dvd n" |"(l::'a::idom) dvd (m * n)") = - \fn phi => Numeral_Simprocs.dvd_cancel_factor\ + \K Numeral_Simprocs.dvd_cancel_factor\ simproc_setup divide_cancel_factor ("((l::'a::field) * m) / n" |"(l::'a::field) / (m * n)") = - \fn phi => Numeral_Simprocs.divide_cancel_factor\ + \K Numeral_Simprocs.divide_cancel_factor\ ML_file \Tools/nat_numeral_simprocs.ML\ simproc_setup nat_combine_numerals ("(i::nat) + j" | "Suc (i + j)") = - \fn phi => Nat_Numeral_Simprocs.combine_numerals\ + \K Nat_Numeral_Simprocs.combine_numerals\ 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") = - \fn phi => Nat_Numeral_Simprocs.eq_cancel_numerals\ + \K Nat_Numeral_Simprocs.eq_cancel_numerals\ 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") = - \fn phi => Nat_Numeral_Simprocs.less_cancel_numerals\ + \K Nat_Numeral_Simprocs.less_cancel_numerals\ simproc_setup natle_cancel_numerals ("(l::nat) + m \ n" | "(l::nat) \ m + n" | "(l::nat) * m \ n" | "(l::nat) \ m * n" | "Suc m \ n" | "m \ Suc n") = - \fn phi => Nat_Numeral_Simprocs.le_cancel_numerals\ + \K Nat_Numeral_Simprocs.le_cancel_numerals\ 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") = - \fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals\ + \K Nat_Numeral_Simprocs.diff_cancel_numerals\ simproc_setup nat_eq_cancel_numeral_factor ("(l::nat) * m = n" | "(l::nat) = m * n") = - \fn phi => Nat_Numeral_Simprocs.eq_cancel_numeral_factor\ + \K Nat_Numeral_Simprocs.eq_cancel_numeral_factor\ simproc_setup nat_less_cancel_numeral_factor ("(l::nat) * m < n" | "(l::nat) < m * n") = - \fn phi => Nat_Numeral_Simprocs.less_cancel_numeral_factor\ + \K Nat_Numeral_Simprocs.less_cancel_numeral_factor\ simproc_setup nat_le_cancel_numeral_factor ("(l::nat) * m <= n" | "(l::nat) <= m * n") = - \fn phi => Nat_Numeral_Simprocs.le_cancel_numeral_factor\ + \K Nat_Numeral_Simprocs.le_cancel_numeral_factor\ simproc_setup nat_div_cancel_numeral_factor ("((l::nat) * m) div n" | "(l::nat) div (m * n)") = - \fn phi => Nat_Numeral_Simprocs.div_cancel_numeral_factor\ + \K Nat_Numeral_Simprocs.div_cancel_numeral_factor\ simproc_setup nat_dvd_cancel_numeral_factor ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") = - \fn phi => Nat_Numeral_Simprocs.dvd_cancel_numeral_factor\ + \K Nat_Numeral_Simprocs.dvd_cancel_numeral_factor\ simproc_setup nat_eq_cancel_factor ("(l::nat) * m = n" | "(l::nat) = m * n") = - \fn phi => Nat_Numeral_Simprocs.eq_cancel_factor\ + \K Nat_Numeral_Simprocs.eq_cancel_factor\ simproc_setup nat_less_cancel_factor ("(l::nat) * m < n" | "(l::nat) < m * n") = - \fn phi => Nat_Numeral_Simprocs.less_cancel_factor\ + \K Nat_Numeral_Simprocs.less_cancel_factor\ simproc_setup nat_le_cancel_factor ("(l::nat) * m <= n" | "(l::nat) <= m * n") = - \fn phi => Nat_Numeral_Simprocs.le_cancel_factor\ + \K Nat_Numeral_Simprocs.le_cancel_factor\ simproc_setup nat_div_cancel_factor ("((l::nat) * m) div n" | "(l::nat) div (m * n)") = - \fn phi => Nat_Numeral_Simprocs.div_cancel_factor\ + \K Nat_Numeral_Simprocs.div_cancel_factor\ simproc_setup nat_dvd_cancel_factor ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") = - \fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor\ + \K Nat_Numeral_Simprocs.dvd_cancel_factor\ declaration \ K (Lin_Arith.add_simprocs diff -r cec875dcc59e -r 300537844bb7 src/HOL/Product_Type.thy --- 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 @@ \ simproc_setup unit_eq ("x::unit") = \ - 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}))) \ free_constructors case_unit for "()" @@ -570,9 +570,9 @@ end; \ simproc_setup case_prod_beta ("case_prod f z") = - \fn _ => fn ctxt => fn ct => beta_proc ctxt (Thm.term_of ct)\ + \K (fn ctxt => fn ct => beta_proc ctxt (Thm.term_of ct))\ simproc_setup case_prod_eta ("case_prod f") = - \fn _ => fn ctxt => fn ct => eta_proc ctxt (Thm.term_of ct)\ + \K (fn ctxt => fn ct => eta_proc ctxt (Thm.term_of ct))\ lemma case_prod_beta': "(\(x,y). f x y) = (\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") = \ - fn _ => fn ctxt => fn ct => + K (fn ctxt => fn ct => (case Thm.term_of ct of S as Const (\<^const_name>\Collect\, Type (\<^type_name>\fun\, [_, T])) $ t => let val (u, _, ps) = HOLogic.strip_ptupleabs t in @@ -1355,7 +1355,7 @@ else NONE) | _ => NONE) end - | _ => NONE) + | _ => NONE)) \ ML_file \Tools/inductive_set.ML\ diff -r cec875dcc59e -r 300537844bb7 src/HOL/Real_Asymp/exp_log_expression.ML --- 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 = diff -r cec875dcc59e -r 300537844bb7 src/HOL/Set.thy --- 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 @@ \ simproc_setup defined_Collect ("{x. P x \ Q x}") = \ - 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})]))) \ lemmas CollectE = CollectD [elim_format] @@ -330,13 +330,11 @@ \ simproc_setup defined_Bex ("\x\A. P x \ Q x") = \ - fn _ => Quantifier1.rearrange_Bex - (fn ctxt => unfold_tac ctxt @{thms Bex_def}) + K (Quantifier1.rearrange_Bex (fn ctxt => unfold_tac ctxt @{thms Bex_def})) \ simproc_setup defined_All ("\x\A. P x \ Q x") = \ - fn _ => Quantifier1.rearrange_Ball - (fn ctxt => unfold_tac ctxt @{thms Ball_def}) + K (Quantifier1.rearrange_Ball (fn ctxt => unfold_tac ctxt @{thms Ball_def})) \ lemma ballI [intro!]: "(\x. x \ A \ P x) \ \x\A. P x" diff -r cec875dcc59e -r 300537844bb7 src/HOL/Statespace/state_space.ML --- 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) = diff -r cec875dcc59e -r 300537844bb7 src/HOL/Tools/BNF/bnf_def.ML --- 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 = diff -r cec875dcc59e -r 300537844bb7 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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; diff -r cec875dcc59e -r 300537844bb7 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- 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>\Let\, _) $ t $ u) = diff -r cec875dcc59e -r 300537844bb7 src/HOL/Tools/BNF/bnf_gfp_grec.ML --- 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); diff -r cec875dcc59e -r 300537844bb7 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- 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))); diff -r cec875dcc59e -r 300537844bb7 src/HOL/Tools/BNF/bnf_lfp_size.ML --- 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 diff -r cec875dcc59e -r 300537844bb7 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- 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) diff -r cec875dcc59e -r 300537844bb7 src/HOL/Tools/Function/function.ML --- 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) diff -r cec875dcc59e -r 300537844bb7 src/HOL/Tools/Lifting/lifting_def.ML --- 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) diff -r cec875dcc59e -r 300537844bb7 src/HOL/Tools/Lifting/lifting_def_code_dt.ML --- 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 diff -r cec875dcc59e -r 300537844bb7 src/HOL/Tools/Lifting/lifting_setup.ML --- 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." diff -r cec875dcc59e -r 300537844bb7 src/HOL/Tools/Quotient/quotient_def.ML --- 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, _), ...} => diff -r cec875dcc59e -r 300537844bb7 src/HOL/Tools/Quotient/quotient_type.ML --- 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 diff -r cec875dcc59e -r 300537844bb7 src/HOL/Tools/Transfer/transfer_bnf.ML --- 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 diff -r cec875dcc59e -r 300537844bb7 src/HOL/Tools/functor.ML --- 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 diff -r cec875dcc59e -r 300537844bb7 src/HOL/Tools/inductive.ML --- 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; diff -r cec875dcc59e -r 300537844bb7 src/HOL/Tools/inductive_set.ML --- 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; diff -r cec875dcc59e -r 300537844bb7 src/HOL/Tools/semiring_normalizer.ML --- 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; diff -r cec875dcc59e -r 300537844bb7 src/HOL/Tools/typedef.ML --- 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) diff -r cec875dcc59e -r 300537844bb7 src/Provers/order_tac.ML --- 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}, diff -r cec875dcc59e -r 300537844bb7 src/Pure/Admin/isabelle_cronjob.scala --- 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 + diff -r cec875dcc59e -r 300537844bb7 src/Pure/Isar/attrib.ML --- 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 ""; -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; diff -r cec875dcc59e -r 300537844bb7 src/Pure/Isar/bundle.ML --- 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; diff -r cec875dcc59e -r 300537844bb7 src/Pure/Isar/code.ML --- 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); diff -r cec875dcc59e -r 300537844bb7 src/Pure/Isar/entity.ML --- 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 diff -r cec875dcc59e -r 300537844bb7 src/Pure/Isar/expression.ML --- 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' = diff -r cec875dcc59e -r 300537844bb7 src/Pure/Isar/generic_target.ML --- 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) = diff -r cec875dcc59e -r 300537844bb7 src/Pure/Isar/isar_cmd.ML --- 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; diff -r cec875dcc59e -r 300537844bb7 src/Pure/Isar/local_theory.ML --- 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); diff -r cec875dcc59e -r 300537844bb7 src/Pure/Isar/locale.ML --- 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; diff -r cec875dcc59e -r 300537844bb7 src/Pure/Isar/method.ML --- 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 => diff -r cec875dcc59e -r 300537844bb7 src/Pure/Isar/spec_rules.ML --- 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; diff -r cec875dcc59e -r 300537844bb7 src/Pure/Isar/token.ML --- 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)); diff -r cec875dcc59e -r 300537844bb7 src/Pure/ex/Def.thy --- 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) diff -r cec875dcc59e -r 300537844bb7 src/Pure/simplifier.ML --- 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 diff -r cec875dcc59e -r 300537844bb7 src/ZF/OrdQuant.thy --- 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 \Setting up the one-point-rule simproc\ simproc_setup defined_rex ("\x[M]. P(x) \ Q(x)") = \ - fn _ => Quantifier1.rearrange_Bex - (fn ctxt => unfold_tac ctxt @{thms rex_def}) + K (Quantifier1.rearrange_Bex (fn ctxt => unfold_tac ctxt @{thms rex_def})) \ simproc_setup defined_rall ("\x[M]. P(x) \ Q(x)") = \ - fn _ => Quantifier1.rearrange_Ball - (fn ctxt => unfold_tac ctxt @{thms rall_def}) + K (Quantifier1.rearrange_Ball (fn ctxt => unfold_tac ctxt @{thms rall_def})) \ end diff -r cec875dcc59e -r 300537844bb7 src/ZF/pair.thy --- 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 \val ZF_ss = simpset_of \<^context>\ simproc_setup defined_Bex ("\x\A. P(x) \ Q(x)") = \ - fn _ => Quantifier1.rearrange_Bex - (fn ctxt => unfold_tac ctxt @{thms Bex_def}) + K (Quantifier1.rearrange_Bex (fn ctxt => unfold_tac ctxt @{thms Bex_def})) \ simproc_setup defined_Ball ("\x\A. P(x) \ Q(x)") = \ - fn _ => Quantifier1.rearrange_Ball - (fn ctxt => unfold_tac ctxt @{thms Ball_def}) + K (Quantifier1.rearrange_Ball (fn ctxt => unfold_tac ctxt @{thms Ball_def})) \