--- a/src/HOLCF/holcf_logic.ML Tue Mar 02 22:20:19 2010 +0100
+++ b/src/HOLCF/holcf_logic.ML Tue Mar 02 23:56:13 2010 +0100
@@ -31,21 +31,14 @@
(* basic types *)
-fun mk_btyp t (S,T) = Type (t,[S,T]);
-
-local
- val intern_type = Sign.intern_type @{theory};
- val u = intern_type "u";
-in
+fun mk_btyp t (S, T) = Type (t, [S, T]);
-val cfun_arrow = intern_type "->";
+val cfun_arrow = @{type_name "->"};
val op ->> = mk_btyp cfun_arrow;
-val mk_ssumT = mk_btyp (intern_type "++");
-val mk_sprodT = mk_btyp (intern_type "**");
-fun mk_uT T = Type (u, [T]);
-val trT = Type (intern_type "tr" , []);
-val oneT = Type (intern_type "one", []);
+val mk_ssumT = mk_btyp (@{type_name "++"});
+val mk_sprodT = mk_btyp (@{type_name "**"});
+fun mk_uT T = Type (@{type_name u}, [T]);
+val trT = @{typ tr};
+val oneT = @{typ one};
end;
-
-end;