# HG changeset patch
# User wenzelm
# Date 1724593207 -7200
# Node ID 47c0aa388621d34f3599b3f07f70155c193080b2
# Parent  29837d4809e7a891bc0f9bd91a029d6ba0a5d39c
tuned: prefer notation for Pure.type;

diff -r 29837d4809e7 -r 47c0aa388621 src/HOL/Analysis/Abstract_Metric_Spaces.thy
--- 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
diff -r 29837d4809e7 -r 47c0aa388621 src/HOL/GCD.thy
--- 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)