src/HOL/Tools/inductive_realizer.ML
changeset 55235 4b4627f5912b
parent 54742 7a86358a3c0b
child 55954 a29aefc88c8d
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat Feb 01 18:40:47 2014 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Feb 01 18:41:48 2014 +0100
     1.3 @@ -14,12 +14,11 @@
     1.4  structure InductiveRealizer : INDUCTIVE_REALIZER =
     1.5  struct
     1.6  
     1.7 -(* FIXME: Local_Theory.note should return theorems with proper names! *)  (* FIXME ?? *)
     1.8  fun name_of_thm thm =
     1.9    (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
    1.10        [Thm.proof_of thm] [] of
    1.11      [name] => name
    1.12 -  | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
    1.13 +  | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
    1.14  
    1.15  fun prf_of thm =
    1.16    Reconstruct.proof_of thm