src/Pure/axclass.ML

--- a/src/Pure/axclass.ML	Mon Jan 08 21:53:27 2024 +0100
+++ b/src/Pure/axclass.ML	Mon Jan 08 21:54:20 2024 +0100
@@ -381,7 +381,7 @@
       | [] => ()
       | _ => error ("Multiple type variables in class axiom:\n" ^ Syntax.string_of_term ctxt t);
       t
-      |> Term.map_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
+      |> (Term.map_types o Term.map_atyps_same) (fn TFree _ => Term.aT [] | _ => raise Same.SAME)
       |> Logic.close_form);
 
     val axiomss = map (map (prep_axiom o Sign.cert_prop thy) o snd) raw_specs;