# HG changeset patch
# User nipkow
# Date 1581883888 -3600
# Node ID efcd6742ea9c908b05ffa4d06ea973b7fe4c7caa
# Parent  404624eb3a22936f25e3e2d59bfe7d989b3316f4# Parent  3cf130a896a393540a445c9f64d9ce02423fbc2c
merged

diff -r 3cf130a896a3 -r efcd6742ea9c NEWS
--- a/NEWS	Sun Feb 16 18:01:03 2020 +0100
+++ b/NEWS	Sun Feb 16 21:11:28 2020 +0100
@@ -36,6 +36,9 @@
 * Refined treatment of proof terms, including type-class proofs for
 minor object-logics (FOL, FOLP, Sequents).
 
+* The inference kernel is now confined to one main module: structure
+Thm, without the former circular dependency on structure Axclass.
+
 
 *** Isar ***
 
diff -r 3cf130a896a3 -r efcd6742ea9c src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Feb 16 18:01:03 2020 +0100
+++ b/src/Pure/thm.ML	Sun Feb 16 21:11:28 2020 +0100
@@ -1694,8 +1694,8 @@
   end |> solve_constraints;
 
 (*Remove extra sorts that are witnessed by type signature information*)
-fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm
-  | strip_shyps (thm as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) =
+fun strip_shyps0 (thm as Thm (_, {shyps = [], ...})) = thm
+  | strip_shyps0 (thm as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) =
       let
         val thy = theory_of_thm thm;
         val algebra = Sign.classes_of thy;
@@ -1705,14 +1705,18 @@
         val witnessed = Sign.witness_sorts thy present extra;
         val extra' = fold (Sorts.remove_sort o #2) witnessed extra
           |> Sorts.minimal_sorts algebra;
+        val constraints' = fold (insert_constraints thy) witnessed constraints;
         val shyps' = fold (Sorts.insert_sort o #2) present extra';
       in
         Thm (deriv_rule_unconditional
           (Proofterm.strip_shyps_proof algebra present witnessed extra') der,
-         {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints,
+         {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints',
           shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
       end;
 
+val strip_shyps = solve_constraints #> strip_shyps0 #> solve_constraints;
+
+
 (*Internalize sort constraints of type variables*)
 val unconstrainT =
   solve_constraints #> (fn thm as Thm (der, args) =>