diff -r c533bec6e92d -r 64ead6de6212 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Thu Jul 25 14:01:06 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Jul 26 09:35:02 2019 +0200
@@ -167,7 +167,7 @@
 fun proof_syntax prf =
   let
     val thm_names = Symtab.keys (Proofterm.fold_proof_atoms true
-      (fn PThm (_, ((name, _, _), _)) => if name <> "" then Symtab.update (name, ()) else I
+      (fn PThm (_, ((name, _, _, _), _)) => if name <> "" then Symtab.update (name, ()) else I
         | _ => I) [prf] Symtab.empty);
     val axm_names = Symtab.keys (Proofterm.fold_proof_atoms true
       (fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty);
@@ -184,7 +184,7 @@
     val prf = Thm.proof_of thm;
     val prf' =
       (case Proofterm.strip_combt (fst (Proofterm.strip_combP prf)) of
-        (PThm (_, ((_, prop', _), body)), _) =>
+        (PThm (_, ((_, prop', _, _), body)), _) =>
           if prop = prop' then Proofterm.join_proof body else prf
       | _ => prf)
   in if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf' end;