--- a/src/HOL/Analysis/Abstract_Metric_Spaces.thy Sun Aug 25 15:16:32 2024 +0200
+++ b/src/HOL/Analysis/Abstract_Metric_Spaces.thy Sun Aug 25 15:40:07 2024 +0200
@@ -1588,7 +1588,7 @@
by (force simp: Cauchy_def Met_TC.MCauchy_def)
lemma mcomplete_iff_complete [iff]:
- "Met_TC.mcomplete (Pure.type ::'a::metric_space itself) \<longleftrightarrow> complete (UNIV::'a set)"
+ "Met_TC.mcomplete TYPE('a::metric_space) \<longleftrightarrow> complete (UNIV::'a set)"
by (auto simp: Met_TC.mcomplete_def complete_def)
context Submetric
--- a/src/HOL/GCD.thy Sun Aug 25 15:16:32 2024 +0200
+++ b/src/HOL/GCD.thy Sun Aug 25 15:40:07 2024 +0200
@@ -2856,7 +2856,7 @@
context
fixes CHAR :: nat
- defines "CHAR \<equiv> semiring_char (Pure.type :: 'a itself)"
+ defines "CHAR \<equiv> semiring_char TYPE('a)"
begin
lemma of_nat_CHAR [simp]: "of_nat CHAR = (0 :: 'a)"
@@ -2929,7 +2929,7 @@
end
end
-lemma (in semiring_char_0) CHAR_eq_0 [simp]: "semiring_char (Pure.type :: 'a itself) = 0"
+lemma (in semiring_char_0) CHAR_eq_0 [simp]: "semiring_char TYPE('a) = 0"
by (simp add: CHAR_eq0_iff)