src/ZF/Tools/cartprod.ML

 (*Bogus product type underlying a (possibly nested) Sigma.  
   Lets us share HOL code*)
 fun pseudo_type (t $ A $ Abs(_,_,B)) = 
       if t = Pr.sigma
       then mk_prod(pseudo_type A, pseudo_type B)
-      else @{typ i}
-  | pseudo_type _ = @{typ i};
+      else \<^typ>\<open>i\<close>
+  | pseudo_type _ = \<^typ>\<open>i\<close>;
 
 (*Maps the type T1*...*Tn to [T1,...,Tn], however nested*)
 fun factors (Type("*", [T1, T2])) = factors T1 @ factors T2
   | factors T                     = [T];