# HG changeset patch
# User wenzelm
# Date 1391276508 -3600
# Node ID 4b4627f5912bcfe3c96a5df15ea1bd11f7d2630e
# Parent  7c6c833069d2bfdbbf483d0572d232353fba8560
more explicit low-level exception;

diff -r 7c6c833069d2 -r 4b4627f5912b src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Sat Feb 01 18:40:47 2014 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Sat Feb 01 18:41:48 2014 +0100
@@ -14,12 +14,11 @@
 structure InductiveRealizer : INDUCTIVE_REALIZER =
 struct
 
-(* FIXME: Local_Theory.note should return theorems with proper names! *)  (* FIXME ?? *)
 fun name_of_thm thm =
   (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
       [Thm.proof_of thm] [] of
     [name] => name
-  | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
+  | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
 
 fun prf_of thm =
   Reconstruct.proof_of thm