src/ZF/Tools/datatype_package.ML

 
   (*** Define the case operator ***)
 
   (*Combine split terms using case; yields the case operator for one part*)
   fun call_case case_list =
-    let fun call_f (free,[]) = Abs("null", \<^typ>\<open>i\<close>, free)
+    let fun call_f (free,[]) = Abs("null", \<^Type>\<open>i\<close>, free)
           | call_f (free,args) =
                 CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
-                            \<^typ>\<open>i\<close>
+                            \<^Type>\<open>i\<close>
                             free
     in  Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list)  end;
 
   (** Generating function variables for the case definition
       Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)

 
   (** Generating function variables for the recursor definition
       Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
 
   (*a recursive call for x is the application rec`x  *)
-  val rec_call = \<^Const>\<open>apply\<close> $ Free ("rec", \<^typ>\<open>i\<close>);
+  val rec_call = \<^Const>\<open>apply\<close> $ Free ("rec", \<^Type>\<open>i\<close>);
 
   (*look back down the "case args" (which have been reversed) to
     determine the de Bruijn index*)
   fun make_rec_call ([], _) arg = error
           "Internal error in datatype (variable name mismatch)"

     | rec_args (_::prems) = rec_args prems;
 
   (*Add an argument position for each occurrence of a recursive set.
     Strictly speaking, the recursive arguments are the LAST of the function
     variable, but they all have type "i" anyway*)
-  fun add_rec_args args' T = (map (fn _ => \<^typ>\<open>i\<close>) args') ---> T
+  fun add_rec_args args' T = (map (fn _ => \<^Type>\<open>i\<close>) args') ---> T
 
   (*Plug in the function variable type needed for the recursor
     as well as the new arguments (recursive calls)*)
   fun rec_ty_elem ((id, T, syn), name, args, prems) =
       let val args' = rec_args prems

 
   val recursor_def =
       Misc_Legacy.mk_defpair
         (recursor_tm,
          \<^Const>\<open>Univ.Vrecursor\<close> $
-           absfree ("rec", \<^typ>\<open>i\<close>) (list_comb (case_const, recursor_cases)));
+           absfree ("rec", \<^Type>\<open>i\<close>) (list_comb (case_const, recursor_cases)));
 
   (* Build the new theory *)
 
   val need_recursor = (not coind andalso recursor_typ <> case_typ);
 

 
 fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy =
   let
     val ctxt = Proof_Context.init_global thy;
     fun read_is strs =
-      map (Syntax.parse_term ctxt #> Type.constraint \<^typ>\<open>i\<close>) strs
+      map (Syntax.parse_term ctxt #> Type.constraint \<^Type>\<open>i\<close>) strs
       |> Syntax.check_terms ctxt;
 
     val rec_tms = read_is srec_tms;
     val con_ty_lists = Ind_Syntax.read_constructs ctxt scon_ty_lists;
     val dom_sum =