--- 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));