src/HOLCF/Tools/Domain/domain_syntax.ML
changeset 35129 ed24ba6f69aa
parent 33807 ce8d2e8bca21
child 35258 8154c5211ddb
--- a/src/HOLCF/Tools/Domain/domain_syntax.ML	Mon Feb 15 15:50:41 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML	Mon Feb 15 17:17:51 2010 +0100
@@ -28,7 +28,7 @@
 open Domain_Library;
 infixr 5 -->; infixr 6 ->>;
 
-fun calc_syntax
+fun calc_syntax  (* FIXME authentic syntax *)
     (definitional : bool)
     (dtypeprod : typ)
     ((dname : string, typevars : typ list), 
@@ -115,7 +115,7 @@
 
     local open Syntax in
     local
-      fun c_ast con mx = Constant (Syntax.const_name mx (Binding.name_of con));
+      fun c_ast con mx = Constant (Binding.name_of con);   (* FIXME proper const syntax *)
       fun expvar n     = Variable ("e"^(string_of_int n));
       fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
                                    (string_of_int m));