# HG changeset patch # User wenzelm # Date 1226862222 -3600 # Node ID 463c9e9111ae896ab23f5150bb74440e8a09045e # Parent ca3f7bb866f3bc1ec61b98607716123dbd0248ad clarified Thm.proof_body_of vs. Thm.proof_of; diff -r ca3f7bb866f3 -r 463c9e9111ae src/HOL/Tools/datatype_realizer.ML --- a/src/HOL/Tools/datatype_realizer.ML Sun Nov 16 18:19:27 2008 +0100 +++ b/src/HOL/Tools/datatype_realizer.ML Sun Nov 16 20:03:42 2008 +0100 @@ -27,8 +27,7 @@ in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end; fun prf_of thm = - Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) - (Proofterm.proof_of (Thm.proof_of thm)); + Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm); fun prf_subst_vars inst = Proofterm.map_proof_terms (subst_vars ([], inst)) I; diff -r ca3f7bb866f3 -r 463c9e9111ae src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Sun Nov 16 18:19:27 2008 +0100 +++ b/src/HOL/Tools/inductive_realizer.ML Sun Nov 16 20:03:42 2008 +0100 @@ -18,7 +18,7 @@ (* FIXME: LocalTheory.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) - [Proofterm.proof_of (Thm.proof_of thm)] [] of + [Thm.proof_of thm] [] of [name] => name | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm)); @@ -27,8 +27,7 @@ fun prf_of thm = let val thy = Thm.theory_of_thm thm; - val thm' = - Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Proofterm.proof_of (Thm.proof_of thm)); + val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm); in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *) fun forall_intr_prf t prf = diff -r ca3f7bb866f3 -r 463c9e9111ae src/HOL/Tools/rewrite_hol_proof.ML --- a/src/HOL/Tools/rewrite_hol_proof.ML Sun Nov 16 18:19:27 2008 +0100 +++ b/src/HOL/Tools/rewrite_hol_proof.ML Sun Nov 16 20:03:42 2008 +0100 @@ -291,8 +291,8 @@ | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f) = SOME (f, ps) | strip_cong _ _ = NONE; -val subst_prf = fst (strip_combt (Proofterm.proof_of (Thm.proof_of subst))); -val sym_prf = fst (strip_combt (Proofterm.proof_of (Thm.proof_of sym))); +val subst_prf = fst (strip_combt (Thm.proof_of subst)); +val sym_prf = fst (strip_combt (Thm.proof_of sym)); fun make_subst Ts prf xs (_, []) = prf | make_subst Ts prf xs (f, ((x, y), prf') :: ps) = diff -r ca3f7bb866f3 -r 463c9e9111ae src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sun Nov 16 18:19:27 2008 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Sun Nov 16 20:03:42 2008 +0100 @@ -469,7 +469,7 @@ let val (ctxt, (_, thm)) = Proof.get_goal state; val thy = ProofContext.theory_of ctxt; - val prf = Proofterm.proof_of (Thm.proof_of thm); + val prf = Thm.proof_of thm; val prop = Thm.full_prop_of thm; val prf' = Proofterm.rewrite_proof_notypes ([], []) prf in diff -r ca3f7bb866f3 -r 463c9e9111ae src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Sun Nov 16 18:19:27 2008 +0100 +++ b/src/Pure/Proof/extraction.ML Sun Nov 16 20:03:42 2008 +0100 @@ -714,7 +714,7 @@ let val thy = Thm.theory_of_thm thm; val prop = Thm.prop_of thm; - val prf = proof_of (Thm.proof_of thm); + val prf = Thm.proof_of thm; val name = Thm.get_name thm; val _ = name <> "" orelse error "extraction: unnamed theorem"; val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^ diff -r ca3f7bb866f3 -r 463c9e9111ae src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Sun Nov 16 18:19:27 2008 +0100 +++ b/src/Pure/Proof/proof_syntax.ML Sun Nov 16 20:03:42 2008 +0100 @@ -109,7 +109,7 @@ | "thm" :: xs => let val name = NameSpace.implode xs; in (case AList.lookup (op =) thms name of - SOME thm => fst (strip_combt (Proofterm.proof_of (Thm.proof_of thm))) + SOME thm => fst (strip_combt (Thm.proof_of thm)) | NONE => error ("Unknown theorem " ^ quote name)) end | _ => error ("Illegal proof constant name: " ^ quote s)) @@ -227,7 +227,7 @@ let val thy = Thm.theory_of_thm thm; val prop = Thm.full_prop_of thm; - val prf = Proofterm.proof_of (Thm.proof_of thm); + val prf = Thm.proof_of thm; val prf' = (case strip_combt (fst (strip_combP prf)) of (PThm (_, ((_, prop', _), body)), _) => if prop = prop' then force_proof body else prf | _ => prf) diff -r ca3f7bb866f3 -r 463c9e9111ae src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Nov 16 18:19:27 2008 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Nov 16 20:03:42 2008 +0100 @@ -254,7 +254,7 @@ thms |> fold (fn (_, ((name, _, _), _)) => name <> "" ? Symtab.update (name, ())); fun add_thm th = - (case Thm.proof_of th of + (case Thm.proof_body_of th of PBody {proof = PThm (_, ((name, _, _), body)), ...} => if Thm.has_name_hint th andalso Thm.get_name_hint th = name then add_proof_body (Lazy.force body) diff -r ca3f7bb866f3 -r 463c9e9111ae src/Pure/Thy/thm_deps.ML --- a/src/Pure/Thy/thm_deps.ML Sun Nov 16 18:19:27 2008 +0100 +++ b/src/Pure/Thy/thm_deps.ML Sun Nov 16 20:03:42 2008 +0100 @@ -23,7 +23,7 @@ fun thm_deps thms = let - val graph = Proofterm.fold_body_thms add_dep (map Thm.proof_of thms) Graph.empty; + val graph = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) Graph.empty; fun add_entry (name, (_, (preds, _))) = let val prefix = #1 (Library.split_last (NameSpace.explode name)); @@ -61,7 +61,7 @@ val tab = Proofterm.fold_body_thms (fn ((name, prop, _), _) => name <> "" ? Symtab.insert_list (op =) (name, prop)) - (map (Proofterm.strip_thm o Thm.proof_of o snd) thms) Symtab.empty; + (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty; fun is_unused (name, th) = not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th)); diff -r ca3f7bb866f3 -r 463c9e9111ae src/Pure/thm.ML --- a/src/Pure/thm.ML Sun Nov 16 18:19:27 2008 +0100 +++ b/src/Pure/thm.ML Sun Nov 16 20:03:42 2008 +0100 @@ -148,7 +148,8 @@ val freezeT: thm -> thm val join_futures: theory -> unit val future: (unit -> thm) -> cterm -> thm - val proof_of: thm -> proof_body + val proof_body_of: thm -> proof_body + val proof_of: thm -> proof val extern_oracles: theory -> xstring list val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory end; @@ -394,9 +395,6 @@ (* basic components *) -fun deriv_of (Thm (Deriv der, _)) = der; -val proof_term_of = Proofterm.proof_of o #body o deriv_of; - val theory_of_thm = Theory.deref o #thy_ref o rep_thm; val maxidx_of = #maxidx o rep_thm; fun maxidx_thm th i = Int.max (maxidx_of th, i); @@ -1660,18 +1658,23 @@ (* fulfilled proof *) -fun proof_of thm = +fun deriv_of (Thm (Deriv der, _)) = der; +val raw_proof_of = Proofterm.proof_of o #body o deriv_of; + +fun proof_body_of thm = let val {all_promises, promises, body} = deriv_of thm; val _ = Exn.release_all (map (Future.join_result o #2) (rev all_promises)); - val ps = map (apsnd (Lazy.value o proof_term_of o Future.join)) promises; + val ps = map (apsnd (Lazy.value o raw_proof_of o Future.join)) promises; in Pt.fulfill_proof ps body end; +val proof_of = Proofterm.proof_of o proof_body_of; + (* closed derivations with official name *) fun get_name thm = - Pt.get_name (hyps_of thm) (prop_of thm) (proof_term_of thm); + Pt.get_name (hyps_of thm) (prop_of thm) (raw_proof_of thm); fun put_name name (thm as Thm (der, args)) = let @@ -1680,7 +1683,7 @@ val _ = null tpairs orelse raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]); val ps = - map (apsnd (fn future => Lazy.lazy (fn () => proof_term_of (Future.join future)))) promises; + map (apsnd (fn future => Lazy.lazy (fn () => raw_proof_of (Future.join future)))) promises; val thy = Theory.deref thy_ref; val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body; val der' = make_deriv [] [] [] [pthm] proof;