# HG changeset patch
# User wenzelm
# Date 1704570830 -3600
# Node ID 4cd892d1a6761e5ca1ef7c8369af69f1f86ba37d
# Parent  6f852d23306a560a62b1180a90b35dc18d771d19
omit syntactic of_class check, which is in conflict with sort constraints within the logic;

diff -r 6f852d23306a -r 4cd892d1a676 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Sat Jan 06 20:41:07 2024 +0100
+++ b/src/Pure/zterm.ML	Sat Jan 06 20:53:50 2024 +0100
@@ -803,10 +803,8 @@
 fun close_prop prems prop =
   fold_rev (fn A => fn B => ZApp (ZApp (ZConst0 "Pure.imp", A), B)) prems prop;
 
-fun close_proof of_class prems prf =
+fun close_proof prems prf =
   let
-    fun err msg t = raise ZTERM (msg, [], [t], [prf]);
-
     val m = length prems - 1;
     val bounds = ZTerms.build (prems |> fold_index (fn (i, h) => ZTerms.update (h, m - i)));
     fun get_bound lev t = ZTerms.lookup bounds t |> Option.map (fn i => ZBoundp (lev + i));
@@ -814,13 +812,11 @@
     fun proof lev (ZHyp t) =
           (case get_bound lev t of
             SOME p => p
-          | NONE => err "Loose bound in proof term" t)
+          | NONE => raise ZTERM ("Loose bound in proof term", [], [t], [prf]))
       | proof lev (ZClassp C) =
           (case get_bound lev (ZClass C) of
             SOME p => p
-          | NONE =>
-              if of_class C then raise Same.SAME
-              else err "Invalid class constraint " (ZClass C))
+          | NONE => raise Same.SAME)
       | proof lev (ZAbst (x, T, p)) = ZAbst (x, T, proof lev p)
       | proof lev (ZAbsp (x, t, p)) = ZAbsp (x, t, proof (lev + 1) p)
       | proof lev (ZAppt (p, t)) = ZAppt (proof lev p, t)
@@ -832,10 +828,7 @@
 
 fun box_proof zproof_name thy hyps concl prf =
   let
-    val {zterm, typ, ...} = norm_cache thy;
-
-    val algebra = Sign.classes_of thy;
-    fun of_class (T, c) = Sorts.of_sort algebra (typ T, [c]);
+    val {zterm, ...} = zterm_cache thy;
 
     val present_set = Types.build (fold Types.add_atyps hyps #> Types.add_atyps concl);
     val ucontext = Logic.unconstrain_context [] present_set;
@@ -865,7 +858,7 @@
     val args = map ZClassp outer_constraints @ map (ZHyp o zterm) hyps;
     val prems = constraints @ map unconstrain_zterm hyps;
     val prop' = beta_norm_term (close_prop prems (unconstrain_zterm concl));
-    val prf' = beta_norm_prooft (close_proof of_class prems (unconstrain_proof prf));
+    val prf' = beta_norm_prooft (close_proof prems (unconstrain_proof prf));
 
     val i = serial ();
     val zbox: zbox = (i, (prop', prf'));