src/HOL/Tools/inductive_realizer.ML

--- a/src/HOL/Tools/inductive_realizer.ML	Thu Jul 25 14:01:06 2019 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Fri Jul 26 09:35:02 2019 +0200
@@ -14,7 +14,7 @@
 struct
 
 fun name_of_thm thm =
-  (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
+  (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _, _), _)) => cons name | _ => I)
       [Thm.proof_of thm] [] of
     [name] => name
   | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));