--- a/src/Pure/Proof/extraction.ML Sun Oct 20 16:16:23 2019 +0200
+++ b/src/Pure/Proof/extraction.ML Sun Oct 20 20:38:22 2019 +0200
@@ -504,9 +504,11 @@
val procs = maps (rev o fst o snd) types;
val rtypes = map fst types;
val typroc = typeof_proc [];
+ fun expand_name ({name, ...}: Proofterm.thm_header) =
+ if name = "" orelse member (op =) expand name then SOME "" else NONE;
val prep = the_default (K I) prep thy' o
Proof_Rewrite_Rules.elim_defs thy' false (map (Thm.transfer thy) defs) o
- Proofterm.expand_proof thy' (map (rpair NONE) ("" :: expand));
+ Proofterm.expand_proof thy' expand_name;
val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
fun find_inst prop Ts ts vs =