--- a/src/HOLCF/domain/syntax.ML Mon Oct 27 10:46:36 1997 +0100
+++ b/src/HOLCF/domain/syntax.ML Mon Oct 27 11:34:33 1997 +0100
@@ -26,11 +26,12 @@
in
val dtype = Type(dname,typevars);
val dtype2 = foldr' (mk_typ "++") (map prod cons');
- val const_rep = (dname^"_rep" , dtype ~> dtype2, NoSyn');
- val const_abs = (dname^"_abs" , dtype2 ~> dtype , NoSyn');
- val const_when = (dname^"_when", foldr (op ~>) ((map when_type cons'),
- dtype ~> freetvar "t"), NoSyn');
- val const_copy = (dname^"_copy", dtypeprod ~> dtype ~> dtype , NoSyn');
+ val dnam = Sign.base_name dname;
+ val const_rep = (dnam^"_rep" , dtype ~> dtype2, NoSyn');
+ val const_abs = (dnam^"_abs" , dtype2 ~> dtype , NoSyn');
+ val const_when = (dnam^"_when", foldr (op ~>) ((map when_type cons'),
+ dtype ~> freetvar "t"), NoSyn');
+ val const_copy = (dnam^"_copy", dtypeprod ~> dtype ~> dtype , NoSyn');
end;
(* ----- constants concerning the constructors, discriminators and selectors ------ *)
@@ -60,8 +61,8 @@
(* ----- constants concerning induction ------------------------------------------- *)
- val const_take = (dname^"_take" , Type("nat",[]) --> dtype ~> dtype, NoSyn');
- val const_finite = (dname^"_finite", dtype-->HOLogic.boolT , NoSyn');
+ val const_take = (dnam^"_take" , Type("nat",[]) --> dtype ~> dtype, NoSyn');
+ val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT , NoSyn');
(* ----- case translation --------------------------------------------------------- *)
@@ -86,7 +87,7 @@
(mapn case1 1 cons')],
mk_appl (Constant "@fapp") [foldl
(fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
- (Constant (dname^"_when"),mapn arg1 1 cons'),
+ (Constant (dnam^"_when"),mapn arg1 1 cons'),
Variable "x"])
end;
end;
@@ -101,23 +102,17 @@
in (* local *)
-fun add_syntax (comp_dname,eqs': ((string * typ list) *
+fun add_syntax (comp_dnam,eqs': ((string * typ list) *
(string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
let
- fun thy_type (dname,tvars) = (dname, length tvars, NoSyn);
- fun thy_arity (dname,tvars) = (dname, map (snd o rep_TFree) tvars, ["pcpo"]);
- val thy_types = map (thy_type o fst) eqs';
- val thy_arities = map (thy_arity o fst) eqs';
- val dtypes = map (Type o fst) eqs';
+ val dtypes = map (Type o fst) eqs';
val funprod = foldr' (mk_typ "*") (map (fn tp => tp ~> tp )dtypes);
val relprod = foldr' (mk_typ "*") (map (fn tp => tp--> tp --> HOLogic.boolT)dtypes);
- val const_copy = (comp_dname^"_copy" ,funprod ~> funprod , NoSyn');
- val const_bisim = (comp_dname^"_bisim" ,relprod --> HOLogic.boolT, NoSyn');
+ val const_copy = (comp_dnam^"_copy" ,funprod ~> funprod , NoSyn');
+ val const_bisim = (comp_dnam^"_bisim" ,relprod --> HOLogic.boolT, NoSyn');
val ctt = map (calc_syntax funprod) eqs';
val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
-in thy'' |> Theory.add_types thy_types
- |> Theory.add_arities_i thy_arities
- |> add_cur_ops_i (flat(map fst ctt))
+in thy'' |> add_cur_ops_i (flat(map fst ctt))
|> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
|> Theory.add_trrules_i (flat(map snd ctt))
end; (* let *)