src/HOLCF/domain/syntax.ML
changeset 2445 51993fea433f
parent 1637 b8a8ae2e5de1
child 2446 c2a9bf6c0948
--- a/src/HOLCF/domain/syntax.ML	Wed Dec 18 15:13:50 1996 +0100
+++ b/src/HOLCF/domain/syntax.ML	Wed Dec 18 15:16:13 1996 +0100
@@ -1,12 +1,11 @@
-(* syntax.ML
-   Author:  David von Oheimb
-   Created: 31-May-95
-   Updated: 16-Aug-95 case translation
-   Updated: 28-Aug-95 corrections for case translation, simultaneous domain equations
-   Copyright 1995 TU Muenchen
+(*  Title:      HOLCF/domain/syntaxd.ML
+    ID:         $Id$
+    Author : David von Oheimb
+    Copyright 1995, 1996 TU Muenchen
+
+syntax generator for domain section
 *)
 
-
 structure Domain_Syntax = struct 
 
 local 
@@ -103,8 +102,8 @@
 fun add_syntax (comp_dname,eqs': ((string * typ list) *
 		(string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
 let
-  fun thy_type  (dname,typevars)  = (dname, length typevars, NoSyn);
-  fun thy_arity (dname,typevars)  = (dname, map (K ["pcpo"]) typevars, ["pcpo"]); 
+  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';