# 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);