# HG changeset patch
# User wenzelm
# Date 1584112370 -3600
# Node ID 4dd5dadfc87dbf37e6838c0567b948aa67c68495
# Parent  b0b16088ccf2f1b5843056cc15fccf498755dc88
some uses of "' " as witness for this feature;

diff -r b0b16088ccf2 -r 4dd5dadfc87d src/Doc/Classes/Setup.thy
--- a/src/Doc/Classes/Setup.thy	Fri Mar 13 16:04:27 2020 +0100
+++ b/src/Doc/Classes/Setup.thy	Fri Mar 13 16:12:50 2020 +0100
@@ -9,9 +9,9 @@
 
 syntax
   "_alpha" :: "type"  ("\<alpha>")
-  "_alpha_ofsort" :: "sort \<Rightarrow> type"  ("\<alpha>()::_" [0] 1000)
+  "_alpha_ofsort" :: "sort \<Rightarrow> type"  ("\<alpha>' ::_" [0] 1000)
   "_beta" :: "type"  ("\<beta>")
-  "_beta_ofsort" :: "sort \<Rightarrow> type"  ("\<beta>()::_" [0] 1000)
+  "_beta_ofsort" :: "sort \<Rightarrow> type"  ("\<beta>' ::_" [0] 1000)
 
 parse_ast_translation \<open>
   let
diff -r b0b16088ccf2 -r 4dd5dadfc87d src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Fri Mar 13 16:04:27 2020 +0100
+++ b/src/HOL/Number_Theory/Cong.thy	Fri Mar 13 16:12:50 2020 +0100
@@ -37,10 +37,10 @@
 context unique_euclidean_semiring
 begin
 
-definition cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  (\<open>(1[_ = _] '(()mod _'))\<close>)
+definition cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  (\<open>(1[_ = _] '(' mod _'))\<close>)
   where "cong b c a \<longleftrightarrow> b mod a = c mod a"
   
-abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  (\<open>(1[_ \<noteq> _] '(()mod _'))\<close>)
+abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  (\<open>(1[_ \<noteq> _] '(' mod _'))\<close>)
   where "notcong b c a \<equiv> \<not> cong b c a"
 
 lemma cong_refl [simp]:
diff -r b0b16088ccf2 -r 4dd5dadfc87d src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Mar 13 16:04:27 2020 +0100
+++ b/src/Pure/pure_thy.ML	Fri Mar 13 16:12:50 2020 +0100
@@ -117,7 +117,7 @@
     ("_type_name",  typ "longid \<Rightarrow> type_name",         Mixfix.mixfix "_"),
     ("_ofsort",     typ "tid_position \<Rightarrow> sort \<Rightarrow> type", mixfix ("_::_", [1000, 0], 1000)),
     ("_ofsort",     typ "tvar_position \<Rightarrow> sort \<Rightarrow> type", mixfix ("_::_", [1000, 0], 1000)),
-    ("_dummy_ofsort", typ "sort \<Rightarrow> type",              mixfix ("'_()::_", [0], 1000)),
+    ("_dummy_ofsort", typ "sort \<Rightarrow> type",              mixfix ("'_' ::_", [0], 1000)),
     ("",            typ "class_name \<Rightarrow> sort",          Mixfix.mixfix "_"),
     ("_class_name", typ "id \<Rightarrow> class_name",            Mixfix.mixfix "_"),
     ("_class_name", typ "longid \<Rightarrow> class_name",        Mixfix.mixfix "_"),
@@ -142,7 +142,7 @@
     ("",            typ "id_position \<Rightarrow> idt",          Mixfix.mixfix "_"),
     ("_idtdummy",   typ "idt",                         Mixfix.mixfix "'_"),
     ("_idtyp",      typ "id_position \<Rightarrow> type \<Rightarrow> idt",  mixfix ("_::_", [], 0)),
-    ("_idtypdummy", typ "type \<Rightarrow> idt",                 mixfix ("'_()::_", [], 0)),
+    ("_idtypdummy", typ "type \<Rightarrow> idt",                 mixfix ("'_' ::_", [], 0)),
     ("",            typ "idt \<Rightarrow> idt",                  Mixfix.mixfix "'(_')"),
     ("",            typ "idt \<Rightarrow> idts",                 Mixfix.mixfix "_"),
     ("_idts",       typ "idt \<Rightarrow> idts \<Rightarrow> idts",         mixfix ("_/ _", [1, 0], 0)),
diff -r b0b16088ccf2 -r 4dd5dadfc87d src/ZF/Bin.thy
--- a/src/ZF/Bin.thy	Fri Mar 13 16:04:27 2020 +0100
+++ b/src/ZF/Bin.thy	Fri Mar 13 16:12:50 2020 +0100
@@ -101,11 +101,11 @@
                                  NCons(bin_mult(v,w),0))"
 
 syntax
-  "_Int0" :: i  (\<open>#()0\<close>)
-  "_Int1" :: i  (\<open>#()1\<close>)
-  "_Int2" :: i  (\<open>#()2\<close>)
-  "_Neg_Int1" :: i  (\<open>#-()1\<close>)
-  "_Neg_Int2" :: i  (\<open>#-()2\<close>)
+  "_Int0" :: i  (\<open>#' 0\<close>)
+  "_Int1" :: i  (\<open>#' 1\<close>)
+  "_Int2" :: i  (\<open>#' 2\<close>)
+  "_Neg_Int1" :: i  (\<open>#-' 1\<close>)
+  "_Neg_Int2" :: i  (\<open>#-' 2\<close>)
 translations
   "#0" \<rightleftharpoons> "CONST integ_of(CONST Pls)"
   "#1" \<rightleftharpoons> "CONST integ_of(CONST Pls BIT 1)"