--- a/src/Pure/Isar/code.ML Mon May 15 16:18:23 2023 +0200
+++ b/src/Pure/Isar/code.ML Mon May 15 19:40:01 2023 +0200
@@ -572,7 +572,7 @@
fun get_abstype_spec thy tyco = case lookup_vs_type_spec thy tyco of
SOME (vs, Abstractor {abs_rep, abstractor, projection, ...}) =>
- (vs, {abs_rep = abs_rep, abstractor = abstractor, projection = projection})
+ (vs, {abs_rep = Thm.transfer thy abs_rep, abstractor = abstractor, projection = projection})
| _ => error ("Not an abstract type: " ^ tyco);
fun get_type_of_constr_or_abstr thy c =
@@ -1017,13 +1017,13 @@
Abstract (snd (constrain_thm thy (fst (typscheme_abs thy abs_thm)) sorts abs_thm), tyco);
fun conclude_cert (Nothing cert_thm) =
- Nothing (Thm.close_derivation \<^here> cert_thm)
+ Nothing (Thm.close_derivation \<^here> cert_thm |> Thm.trim_context)
| conclude_cert (Equations (cert_thm, propers)) =
- Equations (Thm.close_derivation \<^here> cert_thm, propers)
+ Equations (Thm.close_derivation \<^here> cert_thm |> Thm.trim_context, propers)
| conclude_cert (cert as Projection _) =
cert
| conclude_cert (Abstract (abs_thm, tyco)) =
- Abstract (Thm.close_derivation \<^here> abs_thm, tyco);
+ Abstract (Thm.close_derivation \<^here> abs_thm |> Thm.trim_context, tyco);
fun typscheme_of_cert thy (Nothing cert_thm) =
fst (get_head thy cert_thm)
@@ -1060,6 +1060,7 @@
val tyscm = typscheme_of_cert thy cert;
val thms = if null propers then [] else
cert_thm
+ |> Thm.transfer thy
|> Local_Defs.expand [snd (get_head thy cert_thm)]
|> Thm.varifyT_global
|> Conjunction.elim_balanced (length propers);
@@ -1075,7 +1076,7 @@
| equations_of_cert thy (Abstract (abs_thm, tyco)) =
let
val tyscm = typscheme_abs thy abs_thm;
- val (abs, concrete_thm) = concretify_abs thy tyco abs_thm;
+ val (abs, concrete_thm) = concretify_abs thy tyco (Thm.transfer thy abs_thm);
fun abstractions (args, rhs) = (map (pair NONE) args, (SOME abs, rhs));
in
(tyscm, SOME [((abstractions o dest_eqn o Thm.prop_of) concrete_thm,
@@ -1366,7 +1367,8 @@
SOME (tyco, (vs, (abstractor as (abs, (_, ty)), (proj, abs_rep)))) =>
thy
|> modify_specs (register_type
- (tyco, (vs, Abstractor {abstractor = abstractor, projection = proj, abs_rep = abs_rep, more_abstract_functions = []}))
+ (tyco, (vs, Abstractor {abstractor = abstractor, projection = proj,
+ abs_rep = Thm.trim_context abs_rep, more_abstract_functions = []}))
#> register_fun_spec proj
(Proj (Logic.varify_types_global (mk_proj tyco vs ty abs proj), (tyco, abs))))
|> register_tyco_for_plugin tyco
@@ -1423,7 +1425,7 @@
else specs);
fun add_abstract_for (c, (thm, tyco_abs as (tyco, _))) =
- modify_specs (register_fun_spec c (Abstr (Thm.close_derivation \<^here> thm, tyco_abs))
+ modify_specs (register_fun_spec c (Abstr (Thm.close_derivation \<^here> thm |> Thm.trim_context, tyco_abs))
#> map_types (History.modify_entry tyco (add_abstract_function c)))
in