src/HOLCF/ax_ops/thy_ops.ML
changeset 3534 c245c88194ff
parent 2238 c72a23bbe762
child 3621 d3e248853428
--- a/src/HOLCF/ax_ops/thy_ops.ML	Fri Jul 18 13:54:41 1997 +0200
+++ b/src/HOLCF/ax_ops/thy_ops.ML	Fri Jul 18 13:55:09 1997 +0200
@@ -154,7 +154,7 @@
   | syn_decls _ _ [] = [];
 
 fun translate name vars rhs = 
-    Syntax.<-> ((Ast.mk_appl (Constant (mk_internal_name name)) 
+    Syntax.ParsePrintRule ((Ast.mk_appl (Constant (mk_internal_name name)) 
 		 (map Variable vars)), 
 		rhs); 
 
@@ -178,7 +178,7 @@
             |   argnames _ _ = [];
             val names = argnames (ord"A") typ;
         in if names = [] then [] else 
-	    [Syntax.<-> (mk_appl (Constant name) (map Variable names),
+	    [Syntax.ParsePrintRule (mk_appl (Constant name) (map Variable names),
 			 foldl (fn (t,arg) => 
 				(mk_appl (Constant "@fapp") [t,Variable arg]))
 			 (Constant name,names))] 
@@ -207,7 +207,7 @@
 	    val vars = map Variable (case typ of (Type("->" ,[t,_])) =>argnames (ord"A") t
 						 | _ => []);
         in if vars = [] then [] else 
-	    [Syntax.<-> 
+	    [Syntax.ParsePrintRule 
 	     (mk_appl (Constant name) vars,
 	      mk_appl (Constant "@fapp")
 	      [Constant name,