--- a/src/Pure/Isar/class_declaration.ML Sun Nov 03 19:43:59 2019 +0100
+++ b/src/Pure/Isar/class_declaration.ML Sun Nov 03 20:38:08 2019 +0100
@@ -84,6 +84,7 @@
in
Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'')
(fn {context = ctxt, ...} => ALLGOALS (Proof_Context.fact_tac ctxt [thm'']))
+ |> tap (Thm.expose_proof thy)
end;
val some_assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));
@@ -102,8 +103,9 @@
REPEAT (SOMEGOAL
(match_tac ctxt (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
ORELSE' assume_tac ctxt));
- val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (tac o #context);
-
+ val of_class =
+ Goal.prove_sorry_global thy [] [] of_class_prop (tac o #context)
+ |> tap (Thm.expose_proof thy);
in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end;