src/HOLCF/Tools/fixrec.ML

 (*************************************************************************)
 (***************************** building types ****************************)
 (*************************************************************************)
 
 (* ->> is taken from holcf_logic.ML *)
-fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
+fun cfunT (T, U) = Type(@{type_name cfun}, [T, U]);
 
 infixr 6 ->>; val (op ->>) = cfunT;
 
-fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
+fun dest_cfunT (Type(@{type_name cfun}, [T, U])) = (T, U)
   | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
 
 fun maybeT T = Type(@{type_name "maybe"}, [T]);
 
 fun dest_maybeT (Type(@{type_name "maybe"}, [T])) = T

   | tupleT [T] = T
   | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
 
 local
 
-fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U
+fun binder_cfun (Type(@{type_name cfun},[T, U])) = T :: binder_cfun U
   | binder_cfun (Type(@{type_name "fun"},[T, U])) = T :: binder_cfun U
   | binder_cfun _   =  [];
 
-fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U
+fun body_cfun (Type(@{type_name cfun},[T, U])) = body_cfun U
   | body_cfun (Type(@{type_name "fun"},[T, U])) = body_cfun U
   | body_cfun T   =  T;
 
 fun strip_cfun T : typ list * typ =
   (binder_cfun T, body_cfun T);

   in cabs_const (Term.domain_type T, Term.range_type T) $ t end
 
 fun mk_capply (t, u) =
   let val (S, T) =
     case Term.fastype_of t of
-        Type(@{type_name "->"}, [S, T]) => (S, T)
+        Type(@{type_name cfun}, [S, T]) => (S, T)
       | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]);
   in capply_const (S, T) $ t $ u end;
 
 infix 0 ==;  val (op ==) = Logic.mk_equals;
 infix 1 ===; val (op ===) = HOLogic.mk_eq;

       let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
       in pre_build match_name f rhs' (v::vs) taken' end
   | Const(c,T) =>
       let
         val n = Name.variant taken "v";
-        fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs
+        fun result_type (Type(@{type_name cfun},[_,T])) (x::xs) = result_type T xs
           | result_type (Type (@{type_name "fun"},[_,T])) (x::xs) = result_type T xs
           | result_type T _ = T;
         val v = Free(n, result_type T vs);
         val m = Const(match_name c, matchT (T, fastype_of rhs));
         val k = big_lambdas vs rhs;