1.1 --- a/src/HOLCF/domain/syntax.ML	Mon Oct 27 10:46:36 1997 +0100
     1.2 +++ b/src/HOLCF/domain/syntax.ML	Mon Oct 27 11:34:33 1997 +0100
     1.3 @@ -26,11 +26,12 @@
     1.4  in
     1.5    val dtype  = Type(dname,typevars);
     1.6    val dtype2 = foldr' (mk_typ "++") (map prod cons');
     1.7 -  val const_rep  = (dname^"_rep" ,              dtype  ~> dtype2, NoSyn');
     1.8 -  val const_abs  = (dname^"_abs" ,              dtype2 ~> dtype , NoSyn');
     1.9 -  val const_when = (dname^"_when", foldr (op ~>) ((map when_type cons'),
    1.10 -						 dtype ~> freetvar "t"), NoSyn');
    1.11 -  val const_copy = (dname^"_copy", dtypeprod ~> dtype  ~> dtype , NoSyn');
    1.12 +  val dnam = Sign.base_name dname;
    1.13 +  val const_rep  = (dnam^"_rep" ,              dtype  ~> dtype2, NoSyn');
    1.14 +  val const_abs  = (dnam^"_abs" ,              dtype2 ~> dtype , NoSyn');
    1.15 +  val const_when = (dnam^"_when", foldr (op ~>) ((map when_type cons'),
    1.16 +					       	 dtype ~> freetvar "t"), NoSyn');
    1.17 +  val const_copy = (dnam^"_copy", dtypeprod ~> dtype  ~> dtype , NoSyn');
    1.18  end;
    1.19  
    1.20  (* ----- constants concerning the constructors, discriminators and selectors ------ *)
    1.21 @@ -60,8 +61,8 @@
    1.22  
    1.23  (* ----- constants concerning induction ------------------------------------------- *)
    1.24  
    1.25 -  val const_take   = (dname^"_take"  , Type("nat",[]) --> dtype ~> dtype, NoSyn');
    1.26 -  val const_finite = (dname^"_finite", dtype-->HOLogic.boolT	        , NoSyn');
    1.27 +  val const_take   = (dnam^"_take"  , Type("nat",[]) --> dtype ~> dtype, NoSyn');
    1.28 +  val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT	        , NoSyn');
    1.29  
    1.30  (* ----- case translation --------------------------------------------------------- *)
    1.31  
    1.32 @@ -86,7 +87,7 @@
    1.33  				 (mapn case1 1 cons')],
    1.34         mk_appl (Constant "@fapp") [foldl 
    1.35  				 (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
    1.36 -				 (Constant (dname^"_when"),mapn arg1 1 cons'),
    1.37 +				 (Constant (dnam^"_when"),mapn arg1 1 cons'),
    1.38  				 Variable "x"])
    1.39    end;
    1.40  end;
    1.41 @@ -101,23 +102,17 @@
    1.42  
    1.43  in (* local *)
    1.44  
    1.45 -fun add_syntax (comp_dname,eqs': ((string * typ list) *
    1.46 +fun add_syntax (comp_dnam,eqs': ((string * typ list) *
    1.47  		(string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
    1.48  let
    1.49 -  fun thy_type  (dname,tvars)  = (dname, length tvars, NoSyn);
    1.50 -  fun thy_arity (dname,tvars)  = (dname, map (snd o rep_TFree) tvars, ["pcpo"]);
    1.51 -  val thy_types   = map (thy_type  o fst) eqs';
    1.52 -  val thy_arities = map (thy_arity o fst) eqs';
    1.53 -  val dtypes      = map (Type      o fst) eqs';
    1.54 +  val dtypes  = map (Type      o fst) eqs';
    1.55    val funprod = foldr' (mk_typ "*") (map (fn tp => tp ~> tp                  )dtypes);
    1.56    val relprod = foldr' (mk_typ "*") (map (fn tp => tp--> tp --> HOLogic.boolT)dtypes);
    1.57 -  val const_copy   = (comp_dname^"_copy"  ,funprod ~> funprod       , NoSyn');
    1.58 -  val const_bisim  = (comp_dname^"_bisim" ,relprod --> HOLogic.boolT, NoSyn');
    1.59 +  val const_copy   = (comp_dnam^"_copy"  ,funprod ~> funprod       , NoSyn');
    1.60 +  val const_bisim  = (comp_dnam^"_bisim" ,relprod --> HOLogic.boolT, NoSyn');
    1.61    val ctt           = map (calc_syntax funprod) eqs';
    1.62    val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
    1.63 -in thy'' |> Theory.add_types      thy_types
    1.64 -	 |> Theory.add_arities_i  thy_arities
    1.65 -	 |> add_cur_ops_i (flat(map fst ctt))
    1.66 +in thy'' |> add_cur_ops_i (flat(map fst ctt))
    1.67  	 |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
    1.68  	 |> Theory.add_trrules_i (flat(map snd ctt))
    1.69  end; (* let *)