name_of_thm: Proofterm.fold_proof_atoms;
authorwenzelm
Sat Nov 15 21:31:19 2008 +0100 (2008-11-15)
changeset 2880048f7bfebd31d
parent 28799 ee65e7d043fc
child 28801 fc45401bdf6f
name_of_thm: Proofterm.fold_proof_atoms;
Thm.proof_of returns proof_body;
src/HOL/Tools/inductive_realizer.ML
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat Nov 15 21:31:17 2008 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Nov 15 21:31:19 2008 +0100
     1.3 @@ -15,18 +15,20 @@
     1.4  structure InductiveRealizer : INDUCTIVE_REALIZER =
     1.5  struct
     1.6  
     1.7 -(* FIXME: LocalTheory.note should return theorems with proper names! *)
     1.8 +(* FIXME: LocalTheory.note should return theorems with proper names! *)  (* FIXME ?? *)
     1.9  fun name_of_thm thm =
    1.10 -  (case Symtab.dest (Proofterm.thms_of_proof' (Thm.proof_of thm) Symtab.empty) of
    1.11 -     [(name, _)] => name
    1.12 -   | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm));
    1.13 +  (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
    1.14 +      [Proofterm.proof_of (Thm.proof_of thm)] [] of
    1.15 +    [name] => name
    1.16 +  | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm));
    1.17  
    1.18  val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
    1.19  
    1.20  fun prf_of thm =
    1.21    let
    1.22      val thy = Thm.theory_of_thm thm;
    1.23 -    val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
    1.24 +    val thm' =
    1.25 +      Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Proofterm.proof_of (Thm.proof_of thm));
    1.26    in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
    1.27  
    1.28  fun forall_intr_prf t prf =