--- a/src/Pure/Isar/class.ML Sun May 14 12:34:49 2023 +0200
+++ b/src/Pure/Isar/class.ML Sun May 14 13:00:49 2023 +0200
@@ -478,9 +478,11 @@
fun register_subclass (sub, sup) some_dep_morph some_witn export lthy =
let
val thy = Proof_Context.theory_of lthy;
- val intros = (snd o rules thy) sup :: map_filter I
- [Option.map (Drule.export_without_context_open o Element.conclude_witness lthy) some_witn,
- (fst o rules thy) sub];
+ val conclude_witness =
+ Thm.trim_context o Drule.export_without_context_open o Element.conclude_witness lthy;
+ val intros =
+ (snd o rules thy) sup ::
+ map_filter I [Option.map conclude_witness some_witn, (fst o rules thy) sub];
val classrel =
Goal.prove_sorry_global thy [] [] (Logic.mk_classrel (sub, sup))
(fn {context = ctxt, ...} => EVERY (map (TRYALL o resolve_tac ctxt o single) intros));
--- a/src/Pure/Isar/class_declaration.ML Sun May 14 12:34:49 2023 +0200
+++ b/src/Pure/Isar/class_declaration.ML Sun May 14 13:00:49 2023 +0200
@@ -31,6 +31,7 @@
val certT = Thm.trim_context_ctyp o Thm.global_ctyp_of thy;
val cert = Thm.trim_context_cterm o Thm.global_cterm_of thy;
+ val conclude_witness = Thm.trim_context o Element.conclude_witness thy_ctxt;
(* instantiation of canonical interpretation *)
val a_tfree = (Name.aT, base_sort);
@@ -67,13 +68,13 @@
val tac = loc_intro_tac
THEN ALLGOALS (Proof_Context.fact_tac thy_ctxt (sup_axioms @ the_list assm_axiom));
in Element.prove_witness thy_ctxt prop tac end) some_prop;
- val some_axiom = Option.map (Element.conclude_witness thy_ctxt) some_witn;
+ val some_axiom = Option.map conclude_witness some_witn;
(* canonical interpretation *)
val base_morph = inst_morph
$> Morphism.binding_morphism "class_binding" (Binding.prefix false (Class.class_prefix class))
$> Element.satisfy_morphism (the_list some_witn);
- val eq_morph = Element.eq_morphism thy (Class.these_defs thy sups);
+ val eq_morph = Element.eq_morphism thy (Class.these_defs thy sups |> map Thm.trim_context);
(* assm_intro *)
fun prove_assm_intro thm =
--- a/src/Pure/Isar/element.ML Sun May 14 12:34:49 2023 +0200
+++ b/src/Pure/Isar/element.ML Sun May 14 13:00:49 2023 +0200
@@ -275,7 +275,8 @@
Witness (t,
Goal.prove ctxt [] [] (mark_witness t)
(fn _ => resolve_tac ctxt [Drule.protectI] 1 THEN tac)
- |> Thm.close_derivation \<^here>);
+ |> Thm.close_derivation \<^here>
+ |> Thm.trim_context);
local
@@ -290,7 +291,9 @@
(map o map) (fn prop => (mark_witness prop, [])) wit_propss @
[map (rpair []) eq_props];
fun after_qed' thmss =
- let val (wits, eqs) = split_last ((map o map) (Thm.close_derivation \<^here>) thmss);
+ let
+ val (wits, eqs) =
+ split_last ((map o map) (Thm.close_derivation \<^here> #> Thm.trim_context) thmss);
in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
in proof after_qed' propss #> refine_witness end;
@@ -322,7 +325,7 @@
end;
fun conclude_witness ctxt (Witness (_, th)) =
- Goal.conclude th
+ Goal.conclude (Thm.transfer' ctxt th)
|> Raw_Simplifier.norm_hhf_protect ctxt
|> Thm.close_derivation \<^here>;
@@ -359,7 +362,7 @@
fun compose_witness (Witness (_, th)) r =
let
- val th' = Goal.conclude th;
+ val th' = Goal.conclude (Thm.transfer (Thm.theory_of_thm r) th);
val A = Thm.cprem_of r 1;
in
Thm.implies_elim
--- a/src/Pure/Isar/expression.ML Sun May 14 12:34:49 2023 +0200
+++ b/src/Pure/Isar/expression.ML Sun May 14 13:00:49 2023 +0200
@@ -766,15 +766,15 @@
val ((statement, intro, axioms), thy''') =
thy''
|> def_pred binding parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
- val ctxt''' = Proof_Context.init_global thy''';
+ val conclude_witness =
+ Drule.export_without_context o Element.conclude_witness (Proof_Context.init_global thy''');
val ([(_, [intro']), _], thy'''') =
thy'''
|> Sign.qualified_path true binding
|> Global_Theory.note_thmss ""
[((Binding.name introN, []), [([intro], [Locale.intro_add])]),
((Binding.name axiomsN, []),
- [(map (Drule.export_without_context o Element.conclude_witness ctxt''') axioms,
- [])])]
+ [(map conclude_witness axioms, [])])]
||> Sign.restore_naming thy''';
in (SOME statement, SOME intro', axioms, thy'''') end;
in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy'''') end;
@@ -851,6 +851,7 @@
val notes' =
body_elems
+ |> map (Element.transform_ctxt (Morphism.transfer_morphism thy'))
|> map (defines_to_notes pred_ctxt)
|> map (Element.transform_ctxt a_satisfy)
|> (fn elems =>
--- a/src/Pure/Isar/interpretation.ML Sun May 14 12:34:49 2023 +0200
+++ b/src/Pure/Isar/interpretation.ML Sun May 14 13:00:49 2023 +0200
@@ -98,7 +98,8 @@
let
val factss = thms
|> unflat ((map o map) #1 eqnss)
- |> map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) #1 eqnss);
+ |> map2 (map2 (fn b => fn eq =>
+ (b, [([Morphism.thm export (Thm.transfer' ctxt eq)], [])]))) ((map o map) #1 eqnss);
val (eqnss', ctxt') =
fold_map (fn facts => note Thm.theoremK facts #-> abs_def_rule) factss ctxt;
val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]);
--- a/src/Pure/Isar/locale.ML Sun May 14 12:34:49 2023 +0200
+++ b/src/Pure/Isar/locale.ML Sun May 14 13:00:49 2023 +0200
@@ -212,8 +212,10 @@
thy |> Locales.map (Name_Space.define (Context.Theory thy) true
(binding,
mk_locale ((parameters, spec, (apply2 o Option.map) Thm.trim_context intros,
- map Thm.trim_context axioms, hyp_spec),
- ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
+ map Thm.trim_context axioms,
+ map (Element.transform_ctxt Morphism.trim_context_morphism) hyp_spec),
+ ((map (fn decl => (decl, serial ())) syntax_decls,
+ map (fn (a, facts) => ((a, map Attrib.trim_context_fact facts), serial ())) notes),
(map (fn (name, morph) => make_dep (name, (morph, Morphism.identity))) dependencies,
Inttab.empty)))) #> snd);
(* FIXME Morphism.identity *)