--- a/src/Pure/Isar/element.ML Sun Nov 03 20:38:08 2019 +0100
+++ b/src/Pure/Isar/element.ML Mon Nov 04 14:56:49 2019 +0100
@@ -275,7 +275,7 @@
Witness (t,
Goal.prove ctxt [] [] (mark_witness t)
(fn _ => resolve_tac ctxt [Drule.protectI] 1 THEN tac)
- |> Thm.expose_derivation \<^here>);
+ |> Thm.close_derivation \<^here>);
local
@@ -290,7 +290,7 @@
(map o map) (fn prop => (mark_witness prop, [])) wit_propss @
[map (rpair []) eq_props];
fun after_qed' thmss =
- let val (wits, eqs) = split_last ((map o map) (Thm.expose_derivation \<^here>) thmss);
+ let val (wits, eqs) = split_last ((map o map) (Thm.close_derivation \<^here>) thmss);
in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
in proof after_qed' propss #> refine_witness end;
@@ -324,7 +324,7 @@
fun conclude_witness ctxt (Witness (_, th)) =
Goal.conclude th
|> Raw_Simplifier.norm_hhf_protect ctxt
- |> Thm.expose_derivation \<^here>;
+ |> Thm.close_derivation \<^here>;
fun pretty_witness ctxt witn =
let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in