diff -r 3360ea6b659d -r 54b2e5f771da src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Sun Sep 19 21:35:51 2021 +0200
+++ b/src/ZF/ind_syntax.ML	Sun Sep 19 21:37:14 2021 +0200
@@ -18,14 +18,12 @@
 
 (** Abstract syntax definitions for ZF **)
 
-val iT = \<^Type>\<open>i\<close>;
-
 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
 fun mk_all_imp (A,P) =
-    FOLogic.all_const iT $
-      Abs("v", iT, FOLogic.imp $ \<^Const>\<open>mem for \<open>Bound 0\<close> A\<close> $ Term.betapply(P, Bound 0));
+    FOLogic.all_const \<^Type>\<open>i\<close> $
+      Abs("v", \<^Type>\<open>i\<close>, \<^Const>\<open>imp\<close> $ \<^Const>\<open>mem for \<open>Bound 0\<close> A\<close> $ Term.betapply(P, Bound 0));
 
-fun mk_Collect (a, D, t) = \<^Const>\<open>Collect for D\<close> $ absfree (a, iT) t;
+fun mk_Collect (a, D, t) = \<^Const>\<open>Collect for D\<close> $ absfree (a, \<^Type>\<open>i\<close>) t;
 
 (*simple error-checking in the premises of an inductive definition*)
 fun chk_prem rec_hd \<^Const_>\<open>conj for _ _\<close> =
@@ -64,10 +62,10 @@
 
 (*read a constructor specification*)
 fun read_construct ctxt (id: string, sprems, syn: mixfix) =
-    let val prems = map (Syntax.parse_term ctxt #> Type.constraint FOLogic.oT) sprems
+    let val prems = map (Syntax.parse_term ctxt #> Type.constraint \<^Type>\<open>o\<close>) sprems
           |> Syntax.check_terms ctxt
         val args = map (#1 o dest_mem) prems
-        val T = (map (#2 o dest_Free) args) ---> iT
+        val T = (map (#2 o dest_Free) args) ---> \<^Type>\<open>i\<close>
                 handle TERM _ => error
                     "Bad variable in constructor specification"
     in ((id,T,syn), id, args, prems) end;
@@ -91,7 +89,7 @@
 (*Make a datatype's domain: form the union of its set parameters*)
 fun union_params (rec_tm, cs) =
   let val (_,args) = strip_comb rec_tm
-      fun is_ind arg = (type_of arg = iT)
+      fun is_ind arg = (type_of arg = \<^Type>\<open>i\<close>)
   in  case filter is_ind (args @ cs) of
          [] => \<^Const>\<open>zero\<close>
        | u_args => Balanced_Tree.make mk_Un u_args