renamed |-> <-| <-> to Parse/PrintRule;

--- a/src/HOL/datatype.ML	Fri Jul 18 13:54:41 1997 +0200
+++ b/src/HOL/datatype.ML	Fri Jul 18 13:55:09 1997 +0200
@@ -231,7 +231,7 @@
       
       val xrules =
         let val (first_part, scnd_part) = calc_xrules 1 1 cons_list
-        in [Syntax.<-> (("logic", "case x of " ^ first_part),
+        in [Syntax.ParsePrintRule (("logic", "case x of " ^ first_part),
                         ("logic", tname ^ "_case " ^ scnd_part ^ " x"))]
         end;
 

--- 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, 

--- a/src/HOLCF/domain/syntax.ML	Fri Jul 18 13:54:41 1997 +0200
+++ b/src/HOLCF/domain/syntax.ML	Fri Jul 18 13:55:09 1997 +0200
@@ -79,13 +79,15 @@
 	fun arg1 n (con,_,args) = if args = [] then expvar n 
 				  else mk_appl (Constant "LAM ") 
 		 [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
-  in mk_appl (Constant "@case") [Variable "x", foldr'
+  in
+    ParsePrintRule
+      (mk_appl (Constant "@case") [Variable "x", foldr'
 				 (fn (c,cs) => mk_appl (Constant "@case2") [c,cs])
-				 (mapn case1 1 cons')] <->
-     mk_appl (Constant "@fapp") [foldl 
+				 (mapn case1 1 cons')],
+       mk_appl (Constant "@fapp") [foldl 
 				 (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
 				 (Constant (dname^"_when"),mapn arg1 1 cons'),
-				 Variable "x"]
+				 Variable "x"])
   end;
 end;