1.1 --- a/src/HOLCF/domain/syntax.ML	Wed Dec 18 15:13:50 1996 +0100
     1.2 +++ b/src/HOLCF/domain/syntax.ML	Wed Dec 18 15:16:13 1996 +0100
     1.3 @@ -1,12 +1,11 @@
     1.4 -(* syntax.ML
     1.5 -   Author:  David von Oheimb
     1.6 -   Created: 31-May-95
     1.7 -   Updated: 16-Aug-95 case translation
     1.8 -   Updated: 28-Aug-95 corrections for case translation, simultaneous domain equations
     1.9 -   Copyright 1995 TU Muenchen
    1.10 +(*  Title:      HOLCF/domain/syntaxd.ML
    1.11 +    ID:         $Id$
    1.12 +    Author : David von Oheimb
    1.13 +    Copyright 1995, 1996 TU Muenchen
    1.14 +
    1.15 +syntax generator for domain section
    1.16  *)
    1.17  
    1.18 -
    1.19  structure Domain_Syntax = struct 
    1.20  
    1.21  local 
    1.22 @@ -103,8 +102,8 @@
    1.23  fun add_syntax (comp_dname,eqs': ((string * typ list) *
    1.24  		(string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
    1.25  let
    1.26 -  fun thy_type  (dname,typevars)  = (dname, length typevars, NoSyn);
    1.27 -  fun thy_arity (dname,typevars)  = (dname, map (K ["pcpo"]) typevars, ["pcpo"]); 
    1.28 +  fun thy_type  (dname,tvars)  = (dname, length tvars, NoSyn);
    1.29 +  fun thy_arity (dname,tvars)  = (dname, map (snd o rep_TFree) tvars, ["pcpo"]);
    1.30    val thy_types   = map (thy_type  o fst) eqs';
    1.31    val thy_arities = map (thy_arity o fst) eqs';
    1.32    val dtypes      = map (Type      o fst) eqs';