# HG changeset patch
# User wenzelm
# Date 1632250566 -7200
# Node ID e5ff77db6f386bb6d8f2189f6e6ebd58f3655e98
# Parent  1c2c0380d58b7881919be494c165a7807c35e043
clarified antiquotations;

diff -r 1c2c0380d58b -r e5ff77db6f38 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Tue Sep 21 19:42:30 2021 +0200
+++ b/src/HOL/Transitive_Closure.thy	Tue Sep 21 20:56:06 2021 +0200
@@ -1287,12 +1287,12 @@
   val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};
   val rtrancl_trans = @{thm rtrancl_trans};
 
-  fun decomp (\<^const>\<open>Trueprop\<close> $ t) =
+  fun decomp \<^Const_>\<open>Trueprop for t\<close> =
         let
-          fun dec (Const (\<^const_name>\<open>Set.member\<close>, _) $ (Const (\<^const_name>\<open>Pair\<close>, _) $ a $ b) $ rel) =
+          fun dec \<^Const_>\<open>Set.member _ for \<open>\<^Const_>\<open>Pair _ _ for a b\<close>\<close> rel\<close> =
               let
-                fun decr (Const (\<^const_name>\<open>rtrancl\<close>, _ ) $ r) = (r,"r*")
-                  | decr (Const (\<^const_name>\<open>trancl\<close>, _ ) $ r)  = (r,"r+")
+                fun decr \<^Const_>\<open>rtrancl _ for r\<close> = (r,"r*")
+                  | decr \<^Const_>\<open>trancl _ for r\<close> = (r,"r+")
                   | decr r = (r,"r");
                 val (rel,r) = decr (Envir.beta_eta_contract rel);
               in SOME (a,b,rel,r) end
@@ -1312,12 +1312,12 @@
   val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};
   val rtrancl_trans = @{thm rtranclp_trans};
 
-  fun decomp (\<^const>\<open>Trueprop\<close> $ t) =
+  fun decomp \<^Const_>\<open>Trueprop for t\<close> =
         let
           fun dec (rel $ a $ b) =
             let
-              fun decr (Const (\<^const_name>\<open>rtranclp\<close>, _ ) $ r) = (r,"r*")
-                | decr (Const (\<^const_name>\<open>tranclp\<close>, _ ) $ r)  = (r,"r+")
+              fun decr \<^Const_>\<open>rtranclp _ for r\<close> = (r,"r*")
+                | decr \<^Const_>\<open>tranclp _ for r\<close> = (r,"r+")
                 | decr r = (r,"r");
               val (rel,r) = decr rel;
             in SOME (a, b, rel, r) end
diff -r 1c2c0380d58b -r e5ff77db6f38 src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Tue Sep 21 19:42:30 2021 +0200
+++ b/src/HOL/Typerep.thy	Tue Sep 21 20:56:06 2021 +0200
@@ -32,8 +32,7 @@
 
 typed_print_translation \<open>
   let
-    fun typerep_tr' ctxt (*"typerep"*)
-            (Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>itself\<close>, [T]), _]))
+    fun typerep_tr' ctxt (*"typerep"*) \<^Type>\<open>fun \<open>\<^Type>\<open>itself T\<close>\<close> _\<close>
             (Const (\<^const_syntax>\<open>Pure.type\<close>, _) :: ts) =
           Term.list_comb
             (Syntax.const \<^syntax_const>\<open>_TYPEREP\<close> $ Syntax_Phases.term_of_typ ctxt T, ts)
@@ -49,10 +48,9 @@
     val sorts = replicate (Sign.arity_number thy tyco) \<^sort>\<open>typerep\<close>;
     val vs = Name.invent_names Name.context "'a" sorts;
     val ty = Type (tyco, map TFree vs);
-    val lhs = Const (\<^const_name>\<open>typerep\<close>, Term.itselfT ty --> \<^typ>\<open>typerep\<close>)
-      $ Free ("T", Term.itselfT ty);
-    val rhs = \<^term>\<open>Typerep\<close> $ HOLogic.mk_literal tyco
-      $ HOLogic.mk_list \<^typ>\<open>typerep\<close> (map (HOLogic.mk_typerep o TFree) vs);
+    val lhs = \<^Const>\<open>typerep ty\<close> $ Free ("T", Term.itselfT ty);
+    val rhs = \<^Const>\<open>Typerep\<close> $ HOLogic.mk_literal tyco
+      $ HOLogic.mk_list \<^Type>\<open>typerep\<close> (map (HOLogic.mk_typerep o TFree) vs);
     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   in
     thy