# HG changeset patch
# User wenzelm
# Date 1684172401 -7200
# Node ID 904242f46ce1e712649757891299adfd6e96331f
# Parent  2d60172c0ade49ff67d41aff3f5b1f7477a78bbc
more accurate Thm.trim_context / Thm.transfer;

diff -r 2d60172c0ade -r 904242f46ce1 src/Pure/Isar/code.ML
--- 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