# 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