# HG changeset patch # User wenzelm # Date 1570800992 -7200 # Node ID 8f050cc0ec501a1cbdd452044ff0716169250f68 # Parent 1fa55b0873bc0babdd9b2bb605c21a6fc3900bfe clarified signature; diff -r 1fa55b0873bc -r 8f050cc0ec50 src/HOL/Proofs/ex/Proof_Terms.thy --- a/src/HOL/Proofs/ex/Proof_Terms.thy Fri Oct 11 11:16:36 2019 +0200 +++ b/src/HOL/Proofs/ex/Proof_Terms.thy Fri Oct 11 15:36:32 2019 +0200 @@ -23,7 +23,7 @@ val thm = @{thm ex}; (*proof body with digest*) - val body = Proofterm.strip_thm (Thm.proof_body_of thm); + val body = Proofterm.strip_thm_body (Thm.proof_body_of thm); (*proof term only*) val prf = Proofterm.proof_of body; diff -r 1fa55b0873bc -r 8f050cc0ec50 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Oct 11 11:16:36 2019 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Oct 11 15:36:32 2019 +0200 @@ -117,7 +117,7 @@ NONE => NONE | SOME body => let val map_names = (case name_tabs of SOME p => apply2 Symtab.lookup p | NONE => `I SOME) in - SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names (Proofterm.strip_thm body)) + SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names (Proofterm.strip_thm_body body)) handle TOO_MANY () => NONE end) diff -r 1fa55b0873bc -r 8f050cc0ec50 src/Pure/Thy/thm_deps.ML --- a/src/Pure/Thy/thm_deps.ML Fri Oct 11 11:16:36 2019 +0200 +++ b/src/Pure/Thy/thm_deps.ML Fri Oct 11 15:36:32 2019 +0200 @@ -105,7 +105,7 @@ val used = Proofterm.fold_body_thms (fn {name = a, ...} => a <> "" ? Symtab.update (a, ())) - (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms))) + (map Proofterm.strip_thm_body (Thm.proof_bodies_of (map (#1 o #2) new_thms))) Symtab.empty; fun is_unused a = not (Symtab.defined used a); diff -r 1fa55b0873bc -r 8f050cc0ec50 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Fri Oct 11 11:16:36 2019 +0200 +++ b/src/Pure/more_thm.ML Fri Oct 11 15:36:32 2019 +0200 @@ -663,7 +663,7 @@ Logic.unconstrainT (Thm.shyps_of thm) (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm)); in - Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) + Proofterm.strip_thm_proof (Thm.proof_of thm) |> Proofterm.reconstruct_proof thy prop |> Proofterm.expand_proof thy [("", NONE)] |> Proofterm.rew_proof thy diff -r 1fa55b0873bc -r 8f050cc0ec50 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Fri Oct 11 11:16:36 2019 +0200 +++ b/src/Pure/proofterm.ML Fri Oct 11 15:36:32 2019 +0200 @@ -77,7 +77,8 @@ val proof_combP: proof * proof list -> proof val strip_combt: proof -> proof * term option list val strip_combP: proof -> proof * proof list - val strip_thm: proof_body -> proof_body + val strip_thm_proof: proof -> proof + val strip_thm_body: proof_body -> proof_body val map_proof_same: term Same.operation -> typ Same.operation -> (typ * class -> proof) -> proof Same.operation val map_proof_terms_same: term Same.operation -> typ Same.operation -> proof Same.operation @@ -451,7 +452,12 @@ | stripc x = x in stripc (prf, []) end; -fun strip_thm (body as PBody {proof, ...}) = +fun strip_thm_proof proof = + (case fst (strip_combt (fst (strip_combP proof))) of + PThm (_, thm_body) => thm_body_proof_raw thm_body + | _ => proof); + +fun strip_thm_body (body as PBody {proof, ...}) = (case fst (strip_combt (fst (strip_combP proof))) of PThm (_, Thm_Body {body = body', ...}) => Future.join body' | _ => body);