src/HOLCF/ax_ops/thy_ops.ML

       (syn_decls curried sign tl)
   | syn_decls curried sign (_::tl) = syn_decls curried sign tl
   | 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); 
 
 (* generating the translation rules. Called by add_ext_axioms(_i) *)
 local open Ast in 

   | xrules_of true ((name,typ,CMixfix(_))::tail) = 
         let fun argnames n (Type("->" ,[_,t]))= chr n :: argnames (n+1) t
             |   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))] 
         end
     @xrules_of true tail

 	    fun argnames n (Type("*" ,[_,t]))= chr n :: argnames (n+1) t
 	    |   argnames n _ = [chr n];
 	    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, 
 	       case vars of [v] => v
 	                 | args => mk_appl (Constant "@ctuple")