proper antiquotations;
authorwenzelm
Tue Mar 02 23:56:13 2010 +0100 (2010-03-02)
changeset 35426c9b9d4fc270d
parent 35425 d4e747d3a874
child 35427 ad039d29e01c
proper antiquotations;
src/HOLCF/holcf_logic.ML
     1.1 --- a/src/HOLCF/holcf_logic.ML	Tue Mar 02 22:20:19 2010 +0100
     1.2 +++ b/src/HOLCF/holcf_logic.ML	Tue Mar 02 23:56:13 2010 +0100
     1.3 @@ -31,21 +31,14 @@
     1.4  
     1.5  (* basic types *)
     1.6  
     1.7 -fun mk_btyp t (S,T) = Type (t,[S,T]);
     1.8 -
     1.9 -local
    1.10 -  val intern_type = Sign.intern_type @{theory};
    1.11 -  val u = intern_type "u";
    1.12 -in
    1.13 +fun mk_btyp t (S, T) = Type (t, [S, T]);
    1.14  
    1.15 -val cfun_arrow = intern_type "->";
    1.16 +val cfun_arrow = @{type_name "->"};
    1.17  val op ->> = mk_btyp cfun_arrow;
    1.18 -val mk_ssumT = mk_btyp (intern_type "++");
    1.19 -val mk_sprodT = mk_btyp (intern_type "**");
    1.20 -fun mk_uT T = Type (u, [T]);
    1.21 -val trT = Type (intern_type "tr" , []);
    1.22 -val oneT = Type (intern_type "one", []);
    1.23 +val mk_ssumT = mk_btyp (@{type_name "++"});
    1.24 +val mk_sprodT = mk_btyp (@{type_name "**"});
    1.25 +fun mk_uT T = Type (@{type_name u}, [T]);
    1.26 +val trT = @{typ tr};
    1.27 +val oneT = @{typ one};
    1.28  
    1.29  end;
    1.30 -
    1.31 -end;