Class contexts with a raised base sort
======================================

If a class assumption forces the class type variable 'a to a sort finer than the base sort
of the superclasses (by an explicit 'a, which gets the default sort, or by a constant whose
type requires a finer sort), the class gets that finer base sort.  Inside the class context,
facts about inherited class operations then no longer apply: the inherited operations are
registered at the base sort of their own class, so the parameter/constant check and uncheck
rewrites set up by Class.synchronize_class_syntax do not match the class parameters, which
live at the finer sort.  In HOLCF this affects bifinite, predomain and domain themselves
(base sort cpo via approx_chain), and any class whose assumption mentions 'a (default sort
domain).

Run:   isabelle build -D . -c

Unpatched Isabelle2025-2 reports errors at:
  Base_Sort_Main.thy:15   class idem_op_ord   (Type unification failed: Variable 'a::ord not of sort idem_op)
                          (lines 20-33 depend on this class)
  Base_Sort_Annot.thy:18  by (fact order2_trans)  in context preorder2_chain
  Base_Sort_Annot.thy:19  by (fact order2_refl)   in context preorder2_chain
  Base_Sort_HOLCF.thy:14  by (fact below_trans)   in context pointed
  Base_Sort_HOLCF.thy:19  by (fact below_trans)   in context bifinite
  Base_Sort_HOLCF.thy:20  by (fact below_refl)    in context bifinite
  Base_Sort_HOLCF.thy:23  by (fact below_antisym) in lemma (in domain)

With the patch to src/Pure/Isar/class.ML all theories check.
Base_Sort_Main and Base_Sort_Annot need only Main; the session parent is HOLCF for the third.
