# HG changeset patch
# User wenzelm
# Date 1632841745 -7200
# Node ID ba880f3a4e525e69cfbc95443d5b91f9c8b25d09
# Parent  e585e5a906bab3d4bc77f743d0157ce85723dac5
tuned antiquotations;

diff -r e585e5a906ba -r ba880f3a4e52 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Tue Sep 28 17:08:38 2021 +0200
+++ b/src/CCL/Wfd.thy	Tue Sep 28 17:09:05 2021 +0200
@@ -441,7 +441,7 @@
 
 fun is_rigid_prog t =
   (case (Logic.strip_assums_concl t) of
-    \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem _ for a _\<close>\<close>\<close> => null (Term.add_vars a [])
+    \<^Const_>\<open>Trueprop for \<^Const_>\<open>mem _ for a _\<close>\<close> => null (Term.add_vars a [])
   | _ => false)
 
 in
diff -r e585e5a906ba -r ba880f3a4e52 src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Tue Sep 28 17:08:38 2021 +0200
+++ b/src/FOLP/IFOLP.thy	Tue Sep 28 17:09:05 2021 +0200
@@ -612,7 +612,7 @@
 structure Hypsubst = Hypsubst
 (
   (*Take apart an equality judgement; otherwise raise Match!*)
-  fun dest_eq \<^Const_>\<open>Proof for \<open>\<^Const_>\<open>eq _ for t u\<close>\<close> _\<close> = (t, u);
+  fun dest_eq \<^Const_>\<open>Proof for \<^Const_>\<open>eq _ for t u\<close> _\<close> = (t, u);
 
   val imp_intr = @{thm impI}
 
diff -r e585e5a906ba -r ba880f3a4e52 src/HOL/HOLCF/Tools/holcf_library.ML
--- a/src/HOL/HOLCF/Tools/holcf_library.ML	Tue Sep 28 17:08:38 2021 +0200
+++ b/src/HOL/HOLCF/Tools/holcf_library.ML	Tue Sep 28 17:09:05 2021 +0200
@@ -58,7 +58,7 @@
   let
     val T = Term.range_type (Term.fastype_of t)
     val UNIV_const = \<^term>\<open>UNIV :: nat set\<close>
-  in \<^Const>\<open>lub T for \<open>\<^Const>\<open>image \<open>\<^Type>\<open>nat\<close>\<close> T for t UNIV_const\<close>\<close>\<close> end
+  in \<^Const>\<open>lub T for \<^Const>\<open>image \<^Type>\<open>nat\<close> T for t UNIV_const\<close>\<close> end
 
 
 (*** Continuous function space ***)
diff -r e585e5a906ba -r ba880f3a4e52 src/HOL/Hoare/hoare_tac.ML
--- a/src/HOL/Hoare/hoare_tac.ML	Tue Sep 28 17:08:38 2021 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML	Tue Sep 28 17:09:05 2021 +0200
@@ -49,7 +49,7 @@
             Abs (_, T, _) => T
           | Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T);
       in
-        \<^Const>\<open>case_prod T T2 \<open>\<^Type>\<open>bool\<close>\<close> for \<open>absfree (x, T) z\<close>\<close>
+        \<^Const>\<open>case_prod T T2 \<^Type>\<open>bool\<close> for \<open>absfree (x, T) z\<close>\<close>
       end;
 
 (** maps [x1,...,xn] to (x1,...,xn) and types**)
diff -r e585e5a906ba -r ba880f3a4e52 src/HOL/Tools/Argo/argo_real.ML
--- a/src/HOL/Tools/Argo/argo_real.ML	Tue Sep 28 17:08:38 2021 +0200
+++ b/src/HOL/Tools/Argo/argo_real.ML	Tue Sep 28 17:09:05 2021 +0200
@@ -12,25 +12,25 @@
 fun trans_type _ \<^Type>\<open>real\<close> tcx = SOME (Argo_Expr.Real, tcx)
   | trans_type _ _ _ = NONE
 
-fun trans_term f \<^Const_>\<open>uminus \<open>\<^Type>\<open>real\<close>\<close> for t\<close> tcx =
+fun trans_term f \<^Const_>\<open>uminus \<^Type>\<open>real\<close> for t\<close> tcx =
       tcx |> f t |>> Argo_Expr.mk_neg |> SOME
-  | trans_term f \<^Const_>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+  | trans_term f \<^Const_>\<open>plus \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_add2 |> SOME
-  | trans_term f \<^Const_>\<open>minus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+  | trans_term f \<^Const_>\<open>minus \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_sub |> SOME
-  | trans_term f \<^Const_>\<open>times \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+  | trans_term f \<^Const_>\<open>times \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_mul |> SOME
-  | trans_term f \<^Const_>\<open>divide \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+  | trans_term f \<^Const_>\<open>divide \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_div |> SOME
-  | trans_term f \<^Const_>\<open>min \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+  | trans_term f \<^Const_>\<open>min \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_min |> SOME
-  | trans_term f \<^Const_>\<open>max \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+  | trans_term f \<^Const_>\<open>max \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_max |> SOME
-  | trans_term f \<^Const_>\<open>abs \<open>\<^Type>\<open>real\<close>\<close> for t\<close> tcx =
+  | trans_term f \<^Const_>\<open>abs \<^Type>\<open>real\<close> for t\<close> tcx =
       tcx |> f t |>> Argo_Expr.mk_abs |> SOME
-  | trans_term f \<^Const_>\<open>less \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+  | trans_term f \<^Const_>\<open>less \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_lt |> SOME
-  | trans_term f \<^Const_>\<open>less_eq \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+  | trans_term f \<^Const_>\<open>less_eq \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_le |> SOME
   | trans_term _ t tcx =
       (case try HOLogic.dest_number t of
@@ -40,12 +40,12 @@
 
 (* reverse translation *)
 
-fun mk_plus t1 t2 = \<^Const>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
+fun mk_plus t1 t2 = \<^Const>\<open>plus \<^Type>\<open>real\<close> for t1 t2\<close>
 fun mk_sum ts = uncurry (fold_rev mk_plus) (split_last ts)
-fun mk_times t1 t2 = \<^Const>\<open>times \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
-fun mk_divide t1 t2 = \<^Const>\<open>divide \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
-fun mk_le t1 t2 = \<^Const>\<open>less_eq \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
-fun mk_lt t1 t2 = \<^Const>\<open>less \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
+fun mk_times t1 t2 = \<^Const>\<open>times \<^Type>\<open>real\<close> for t1 t2\<close>
+fun mk_divide t1 t2 = \<^Const>\<open>divide \<^Type>\<open>real\<close> for t1 t2\<close>
+fun mk_le t1 t2 = \<^Const>\<open>less_eq \<^Type>\<open>real\<close> for t1 t2\<close>
+fun mk_lt t1 t2 = \<^Const>\<open>less \<^Type>\<open>real\<close> for t1 t2\<close>
 
 fun mk_real_num i = HOLogic.mk_number \<^Type>\<open>real\<close> i
 
@@ -54,17 +54,17 @@
   in if q = 1 then mk_real_num p else mk_divide (mk_real_num p) (mk_real_num q) end
 
 fun term_of _ (Argo_Expr.E (Argo_Expr.Num n, _)) = SOME (mk_number n)
-  | term_of f (Argo_Expr.E (Argo_Expr.Neg, [e])) = SOME \<^Const>\<open>uminus \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e\<close>\<close>
+  | term_of f (Argo_Expr.E (Argo_Expr.Neg, [e])) = SOME \<^Const>\<open>uminus \<^Type>\<open>real\<close> for \<open>f e\<close>\<close>
   | term_of f (Argo_Expr.E (Argo_Expr.Add, es)) = SOME (mk_sum (map f es))
   | term_of f (Argo_Expr.E (Argo_Expr.Sub, [e1, e2])) =
-      SOME \<^Const>\<open>minus \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
+      SOME \<^Const>\<open>minus \<^Type>\<open>real\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
   | term_of f (Argo_Expr.E (Argo_Expr.Mul, [e1, e2])) = SOME (mk_times (f e1) (f e2))
   | term_of f (Argo_Expr.E (Argo_Expr.Div, [e1, e2])) = SOME (mk_divide (f e1) (f e2))
   | term_of f (Argo_Expr.E (Argo_Expr.Min, [e1, e2])) =
-      SOME \<^Const>\<open>min \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
+      SOME \<^Const>\<open>min \<^Type>\<open>real\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
   | term_of f (Argo_Expr.E (Argo_Expr.Max, [e1, e2])) =
-      SOME \<^Const>\<open>max \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
-  | term_of f (Argo_Expr.E (Argo_Expr.Abs, [e])) = SOME \<^Const>\<open>abs \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e\<close>\<close>
+      SOME \<^Const>\<open>max \<^Type>\<open>real\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
+  | term_of f (Argo_Expr.E (Argo_Expr.Abs, [e])) = SOME \<^Const>\<open>abs \<^Type>\<open>real\<close> for \<open>f e\<close>\<close>
   | term_of f (Argo_Expr.E (Argo_Expr.Le, [e1, e2])) = SOME (mk_le (f e1) (f e2))
   | term_of f (Argo_Expr.E (Argo_Expr.Lt, [e1, e2])) = SOME (mk_lt (f e1) (f e2))
   | term_of _ _ = NONE
@@ -97,10 +97,10 @@
 
 local
 
-fun is_add2 \<^Const_>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for _ _\<close> = true
+fun is_add2 \<^Const_>\<open>plus \<^Type>\<open>real\<close> for _ _\<close> = true
   | is_add2 _ = false
 
-fun is_add3 \<^Const_>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for _ t\<close> = is_add2 t
+fun is_add3 \<^Const_>\<open>plus \<^Type>\<open>real\<close> for _ t\<close> = is_add2 t
   | is_add3 _ = false
 
 val flatten_thm = mk_rewr @{lemma "(a::real) + b + c = a + (b + c)" by simp}
diff -r e585e5a906ba -r ba880f3a4e52 src/HOL/Tools/Argo/argo_tactic.ML
--- a/src/HOL/Tools/Argo/argo_tactic.ML	Tue Sep 28 17:08:38 2021 +0200
+++ b/src/HOL/Tools/Argo/argo_tactic.ML	Tue Sep 28 17:09:05 2021 +0200
@@ -600,7 +600,7 @@
 
 fun unclausify (thm, lits) ls =
   (case (Thm.prop_of thm, lits) of
-    (\<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>False\<close>\<close>\<close>, [(_, ct)]) =>
+    (\<^Const_>\<open>Trueprop for \<^Const_>\<open>False\<close>\<close>, [(_, ct)]) =>
       let val thm = Thm.implies_intr ct thm
       in (discharge thm unclausify_rule1 handle THM _ => discharge thm unclausify_rule2, ls) end
   | _ => (thm, Ord_List.union lit_ord lits ls))
diff -r e585e5a906ba -r ba880f3a4e52 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Tue Sep 28 17:08:38 2021 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Tue Sep 28 17:09:05 2021 +0200
@@ -261,9 +261,9 @@
 fun refl_clause_aux 0 th = th
   | refl_clause_aux n th =
        case HOLogic.dest_Trueprop (Thm.concl_of th) of
-          \<^Const_>\<open>disj for \<open>\<^Const_>\<open>disj for _ _\<close>\<close> _\<close> =>
+          \<^Const_>\<open>disj for \<^Const_>\<open>disj for _ _\<close> _\<close> =>
             refl_clause_aux n (th RS disj_assoc)    (*isolate an atom as first disjunct*)
-        | \<^Const_>\<open>disj for \<open>\<^Const_>\<open>Not for \<open>\<^Const_>\<open>HOL.eq _ for t u\<close>\<close>\<close>\<close> _\<close> =>
+        | \<^Const_>\<open>disj for \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq _ for t u\<close>\<close> _\<close> =>
             if eliminable(t,u)
             then refl_clause_aux (n-1) (th RS not_refl_disj_D)  (*Var inequation: delete*)
             else refl_clause_aux (n-1) (th RS disj_comm)  (*not between Vars: ignore*)
@@ -271,7 +271,7 @@
         | _ => (*not a disjunction*) th;
 
 fun notequal_lits_count \<^Const_>\<open>disj for P Q\<close> = notequal_lits_count P + notequal_lits_count Q
-  | notequal_lits_count \<^Const_>\<open>Not for \<open>\<^Const_>\<open>HOL.eq _ for _ _\<close>\<close>\<close> = 1
+  | notequal_lits_count \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq _ for _ _\<close>\<close> = 1
   | notequal_lits_count _ = 0;
 
 (*Simplify a clause by applying reflexivity to its negated equality literals*)
@@ -414,7 +414,7 @@
 
 (**** Generation of contrapositives ****)
 
-fun is_left \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>disj for \<open>\<^Const_>\<open>disj for _ _\<close>\<close> _\<close>\<close>\<close> = true
+fun is_left \<^Const_>\<open>Trueprop for \<^Const_>\<open>disj for \<^Const_>\<open>disj for _ _\<close> _\<close>\<close> = true
   | is_left _ = false;
 
 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
@@ -435,7 +435,7 @@
 
 fun rigid t = not (is_Var (head_of t));
 
-fun ok4horn \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>disj for t _\<close>\<close>\<close> = rigid t
+fun ok4horn \<^Const_>\<open>Trueprop for \<^Const_>\<open>disj for t _\<close>\<close> = rigid t
   | ok4horn \<^Const_>\<open>Trueprop for t\<close> = rigid t
   | ok4horn _ = false;
 
@@ -470,7 +470,7 @@
 
 (***** MESON PROOF PROCEDURE *****)
 
-fun rhyps (\<^Const_>\<open>Pure.imp for \<open>\<^Const_>\<open>Trueprop for A\<close>\<close> phi\<close>, As) = rhyps(phi, A::As)
+fun rhyps (\<^Const_>\<open>Pure.imp for \<^Const_>\<open>Trueprop for A\<close> phi\<close>, As) = rhyps(phi, A::As)
   | rhyps (_, As) = As;
 
 (** Detecting repeated assumptions in a subgoal **)
@@ -514,7 +514,7 @@
 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
                not_impD, not_iffD, not_allD, not_exD, not_notD];
 
-fun ok4nnf \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>Not for t\<close>\<close>\<close> = rigid t
+fun ok4nnf \<^Const_>\<open>Trueprop for \<^Const_>\<open>Not for t\<close>\<close> = rigid t
   | ok4nnf \<^Const_>\<open>Trueprop for t\<close> = rigid t
   | ok4nnf _ = false;
 
@@ -620,7 +620,7 @@
 (* Strengthens "f g ~= f h" to "f g ~= f h & (EX x. g x ~= h x)". *)
 fun cong_extensionalize_thm ctxt th =
   (case Thm.concl_of th of
-    \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>Not for \<open>\<^Const_>\<open>HOL.eq T for \<open>t as _ $ _\<close> \<open>u as _ $ _\<close>\<close>\<close>\<close>\<close>\<close> =>
+    \<^Const_>\<open>Trueprop for \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq T for \<open>t as _ $ _\<close> \<open>u as _ $ _\<close>\<close>\<close>\<close> =>
       (case get_F_pattern T t u of
         SOME p => th RS infer_instantiate ctxt [(("F", 0), Thm.cterm_of ctxt p)] ext_cong_neq
       | NONE => th)
diff -r e585e5a906ba -r ba880f3a4e52 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Tue Sep 28 17:08:38 2021 +0200
+++ b/src/HOL/Transitive_Closure.thy	Tue Sep 28 17:09:05 2021 +0200
@@ -1289,7 +1289,7 @@
 
   fun decomp \<^Const_>\<open>Trueprop for t\<close> =
         let
-          fun dec \<^Const_>\<open>Set.member _ for \<open>\<^Const_>\<open>Pair _ _ for a b\<close>\<close> rel\<close> =
+          fun dec \<^Const_>\<open>Set.member _ for \<^Const_>\<open>Pair _ _ for a b\<close> rel\<close> =
               let
                 fun decr \<^Const_>\<open>rtrancl _ for r\<close> = (r,"r*")
                   | decr \<^Const_>\<open>trancl _ for r\<close> = (r,"r+")
diff -r e585e5a906ba -r ba880f3a4e52 src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Tue Sep 28 17:08:38 2021 +0200
+++ b/src/HOL/Typerep.thy	Tue Sep 28 17:09:05 2021 +0200
@@ -32,7 +32,7 @@
 
 typed_print_translation \<open>
   let
-    fun typerep_tr' ctxt (*"typerep"*) \<^Type>\<open>fun \<open>\<^Type>\<open>itself T\<close>\<close> _\<close>
+    fun typerep_tr' ctxt (*"typerep"*) \<^Type>\<open>fun \<^Type>\<open>itself T\<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)
diff -r e585e5a906ba -r ba880f3a4e52 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Tue Sep 28 17:08:38 2021 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Tue Sep 28 17:09:05 2021 +0200
@@ -298,7 +298,7 @@
      (*Used to make induction rules;
         ind_alist = [(rec_tm1,pred1),...] associates predicates with rec ops
         prem is a premise of an intr rule*)
-     fun add_induct_prem ind_alist (prem as \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for t X\<close>\<close>\<close>, iprems) =
+     fun add_induct_prem ind_alist (prem as \<^Const_>\<open>Trueprop for \<^Const_>\<open>mem for t X\<close>\<close>, iprems) =
           (case AList.lookup (op aconv) ind_alist X of
                SOME pred => prem :: \<^make_judgment> (pred $ t) :: iprems
              | NONE => (*possibly membership in M(rec_tm), for M monotone*)
@@ -391,7 +391,7 @@
                             elem_factors ---> \<^Type>\<open>o\<close>)
            val qconcl =
              fold_rev (FOLogic.mk_all o Term.dest_Free) elem_frees
-               \<^Const>\<open>imp for \<open>\<^Const>\<open>mem for elem_tuple rec_tm\<close>\<close> \<open>list_comb (pfree, elem_frees)\<close>\<close>
+               \<^Const>\<open>imp for \<^Const>\<open>mem for elem_tuple rec_tm\<close> \<open>list_comb (pfree, elem_frees)\<close>\<close>
        in  (CP.ap_split elem_type \<^Type>\<open>o\<close> pfree,
             qconcl)
        end;
@@ -400,7 +400,7 @@
 
      (*Used to form simultaneous induction lemma*)
      fun mk_rec_imp (rec_tm,pred) =
-         \<^Const>\<open>imp for \<open>\<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close>\<close> \<open>pred $ Bound 0\<close>\<close>;
+         \<^Const>\<open>imp for \<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close> \<open>pred $ Bound 0\<close>\<close>;
 
      (*To instantiate the main induction rule*)
      val induct_concl =
diff -r e585e5a906ba -r ba880f3a4e52 src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Tue Sep 28 17:08:38 2021 +0200
+++ b/src/ZF/Tools/typechk.ML	Tue Sep 28 17:09:05 2021 +0200
@@ -76,7 +76,7 @@
          if length rls <= maxr then resolve_tac ctxt rls i else no_tac
       end);
 
-fun is_rigid_elem \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for a _\<close>\<close>\<close> = not (is_Var (head_of a))
+fun is_rigid_elem \<^Const_>\<open>Trueprop for \<^Const_>\<open>mem for a _\<close>\<close> = not (is_Var (head_of a))
   | is_rigid_elem _ = false;
 
 (*Try solving a:A by assumption provided a is rigid!*)
diff -r e585e5a906ba -r ba880f3a4e52 src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Tue Sep 28 17:08:38 2021 +0200
+++ b/src/ZF/arith_data.ML	Tue Sep 28 17:09:05 2021 +0200
@@ -48,7 +48,7 @@
 (*Use <-> or = depending on the type of t*)
 fun mk_eq_iff(t,u) =
   if fastype_of t = \<^Type>\<open>i\<close>
-  then \<^Const>\<open>IFOL.eq \<open>\<^Type>\<open>i\<close>\<close> for t u\<close>
+  then \<^Const>\<open>IFOL.eq \<^Type>\<open>i\<close> for t u\<close>
   else \<^Const>\<open>IFOL.iff for t u\<close>;
 
 (*We remove equality assumptions because they confuse the simplifier and
diff -r e585e5a906ba -r ba880f3a4e52 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Tue Sep 28 17:08:38 2021 +0200
+++ b/src/ZF/ind_syntax.ML	Tue Sep 28 17:09:05 2021 +0200
@@ -22,7 +22,7 @@
 fun mk_all_imp (A,P) =
   let val T = \<^Type>\<open>i\<close> in
     \<^Const>\<open>All T for
-      \<open>Abs ("v", T, \<^Const>\<open>imp for \<open>\<^Const>\<open>mem for \<open>Bound 0\<close> A\<close>\<close> \<open>Term.betapply (P, Bound 0)\<close>\<close>)\<close>\<close>
+      \<open>Abs ("v", T, \<^Const>\<open>imp for \<^Const>\<open>mem for \<open>Bound 0\<close> A\<close> \<open>Term.betapply (P, Bound 0)\<close>\<close>)\<close>\<close>
   end;
 
 fun mk_Collect (a, D, t) = \<^Const>\<open>Collect for D\<close> $ absfree (a, \<^Type>\<open>i\<close>) t;
@@ -37,7 +37,7 @@
 
 (*Return the conclusion of a rule, of the form t:X*)
 fun rule_concl rl =
-    let val \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for t X\<close>\<close>\<close> = Logic.strip_imp_concl rl
+    let val \<^Const_>\<open>Trueprop for \<^Const_>\<open>mem for t X\<close>\<close> = Logic.strip_imp_concl rl
     in  (t,X)  end;
 
 (*As above, but return error message if bad*)