src/Pure/Proof/proof_rewrite_rules.ML

     val defnames = map Thm.derivation_name defs;
     val prf' =
       if r then
         let
           val cnames = map (fst o dest_Const o fst) defs';
-          val thms = Proofterm.fold_proof_atoms true
-            (fn PThm ({name, prop, ...}, _) =>
+          val expand = Proofterm.fold_proof_atoms true
+            (fn PThm ({serial, name, prop, ...}, _) =>
                 if member (op =) defnames name orelse
                   not (exists_Const (member (op =) cnames o #1) prop)
                 then I
-                else cons (name, SOME prop)
-              | _ => I) [prf] [];
-        in Proofterm.expand_proof thy thms prf end
+                else Inttab.update (serial, "")
+              | _ => I) [prf] Inttab.empty;
+        in Proofterm.expand_proof thy (Inttab.lookup expand o #serial) prf end
       else prf;
   in
     rewrite_terms (Pattern.rewrite_term thy defs' [])
       (fst (insert_refl defnames [] prf'))
   end;

       (fn T as TVar (ai, _) => TVar (ai, get_sort T)
         | T as TFree (a, _) => TFree (a, get_sort T));
 
     fun reconstruct prop =
       Proofterm.reconstruct_proof thy prop #>
-      Proofterm.expand_proof thy [("", NONE)] #>
+      Proofterm.expand_proof thy Proofterm.expand_name_empty #>
       Same.commit (Proofterm.map_proof_same Same.same Same.same of_class_index);
   in
     map2 reconstruct (Logic.mk_of_sort (T, S))
       (Proofterm.of_sort_proof (Sign.classes_of thy) (Thm.classrel_proof thy) (Thm.arity_proof thy)
         (OfClass o apfst Type.strip_sorts) (subst T, S))