Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more explicit low-level exception;
authorwenzelm
Sat, 01 Feb 2014 18:41:48 +0100
changeset 55235 4b4627f5912b
parent 55234 7c6c833069d2
child 55236 8d61b0aa7a0d
more explicit low-level exception;
src/HOL/Tools/inductive_realizer.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle