# HG changeset patch
# User wenzelm
# Date 1267570573 -3600
# Node ID c9b9d4fc270d8a069e28c1af5f18af85a93e0275
# Parent  d4e747d3a87472ab21e7bd4e414b3eb2c7e91445
proper antiquotations;

diff -r d4e747d3a874 -r c9b9d4fc270d src/HOLCF/holcf_logic.ML
--- 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;