# HG changeset patch
# User wenzelm
# Date 1121362105 -7200
# Node ID 8ff9a80f3c936dd98cd3322e85f7a4ad681f176d
# Parent  5979c46853d1f9f936d1f180ce72a4de577ef22a
removed mk_prodT, mk_not (cf. HOL/hologic.ML);
tuned;

diff -r 5979c46853d1 -r 8ff9a80f3c93 src/HOLCF/holcf_logic.ML
--- a/src/HOLCF/holcf_logic.ML	Thu Jul 14 19:28:24 2005 +0200
+++ b/src/HOLCF/holcf_logic.ML	Thu Jul 14 19:28:25 2005 +0200
@@ -10,52 +10,45 @@
 signature HOLCF_LOGIC =
 sig
   val mk_btyp: string -> typ * typ -> typ
-  val mk_prodT:          typ * typ -> typ
-  val mk_not:  term -> term
-
-  val HOLCF_sg: Sign.sg
   val pcpoC: class
   val pcpoS: sort
   val mk_TFree: string -> typ
   val cfun_arrow: string
-  val ->>      : typ * typ -> typ
-  val mk_ssumT : typ * typ -> typ
+  val ->> : typ * typ -> typ
+  val mk_ssumT: typ * typ -> typ
   val mk_sprodT: typ * typ -> typ
   val mk_uT: typ -> typ
   val trT: typ
   val oneT: typ
-
 end;
 
-
 structure HOLCFLogic: HOLCF_LOGIC =
 struct
 
-open HOLogic;
+(* sort pcpo *)
+
+val pcpoC = Sign.intern_class (the_context ()) "pcpo";
+val pcpoS = [pcpoC];
+fun mk_TFree s = TFree ("'" ^ s, pcpoS);
+
+
+(* basic types *)
 
 fun mk_btyp t (S,T) = Type (t,[S,T]);
-val mk_prodT = mk_btyp "*";
 
-fun mk_not P  = Const ("Not", boolT --> boolT) $ P;
-
-(* basics *)
-
-val HOLCF_sg    = sign_of HOLCF.thy;
-val pcpoC       = Sign.intern_class HOLCF_sg "pcpo";
-val pcpoS       = [pcpoC];
-fun mk_TFree s  = TFree ("'"^s, pcpoS);
+local
+  val intern_type = Sign.intern_type (the_context ());
+  val u = intern_type "u";
+in
 
-(*cfun, ssum, sprod, u, tr, one *)
+val cfun_arrow = intern_type "->";
+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", []);
 
-local val intern = Sign.intern_type HOLCF_sg;
-in
-val cfun_arrow = intern "->";
-val op   ->>  = mk_btyp cfun_arrow;
-val mk_ssumT  = mk_btyp (intern "++");
-val mk_sprodT = mk_btyp (intern "**");
-fun mk_uT T   = Type (intern "u"  ,[T]);
-val trT       = Type (intern "tr" ,[ ]);
-val oneT      = Type (intern "one",[ ]);
 end;
 
 end;