src/Pure/Proof/extraction.ML

--- a/src/Pure/Proof/extraction.ML	Fri Oct 11 19:35:59 2019 +0200
+++ b/src/Pure/Proof/extraction.ML	Fri Oct 11 21:23:06 2019 +0200
@@ -529,7 +529,7 @@
       Logic.mk_of_sort (TVar (ixn, []), Sign.defaultS thy)) tye;
 
     fun mk_sprfs cs tye = maps (fn (_, T) =>
-      ProofRewriteRules.mk_of_sort_proof thy' (map SOME cs)
+      ProofRewriteRules.expand_of_sort_proof thy' (map SOME cs)
         (T, Sign.defaultS thy)) tye;
 
     fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);