# HG changeset patch
# User wenzelm
# Date 1583764732 -3600
# Node ID 046cf49162a3f8de3955ba8f96787841baccbfb0
# Parent  dd56597e026b00fcd9c2b89e9730410cae03fbfe
more thorough strip_shyps for proof boxes (but types are usually stripped and reconstructed later);

diff -r dd56597e026b -r 046cf49162a3 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Mar 09 14:30:09 2020 +0100
+++ b/src/Pure/thm.ML	Mon Mar 09 15:38:52 2020 +0100
@@ -1065,7 +1065,7 @@
   | thm_deps thm = raise THM ("thm_deps: bad promises", 0, [thm]);
 
 fun name_derivation name_pos =
-  solve_constraints #> (fn thm as Thm (der, args) =>
+  strip_shyps #> (fn thm as Thm (der, args) =>
     let
       val thy = theory_of_thm thm;
 
@@ -1734,7 +1734,7 @@
 
 (*Internalize sort constraints of type variables*)
 val unconstrainT =
-  solve_constraints #> (fn thm as Thm (der, args) =>
+  strip_shyps #> (fn thm as Thm (der, args) =>
     let
       val Deriv {promises, body} = der;
       val {cert, shyps, hyps, tpairs, prop, ...} = args;