renamed |-> <-| <-> to Parse/PrintRule;
authorwenzelm
Fri Jul 18 13:55:09 1997 +0200 (1997-07-18)
changeset 3534c245c88194ff
parent 3533 b976967a92fc
child 3535 19bd6c8274c4
renamed |-> <-| <-> to Parse/PrintRule;
src/HOL/datatype.ML
src/HOLCF/ax_ops/thy_ops.ML
src/HOLCF/domain/syntax.ML
     1.1 --- a/src/HOL/datatype.ML	Fri Jul 18 13:54:41 1997 +0200
     1.2 +++ b/src/HOL/datatype.ML	Fri Jul 18 13:55:09 1997 +0200
     1.3 @@ -231,7 +231,7 @@
     1.4        
     1.5        val xrules =
     1.6          let val (first_part, scnd_part) = calc_xrules 1 1 cons_list
     1.7 -        in [Syntax.<-> (("logic", "case x of " ^ first_part),
     1.8 +        in [Syntax.ParsePrintRule (("logic", "case x of " ^ first_part),
     1.9                          ("logic", tname ^ "_case " ^ scnd_part ^ " x"))]
    1.10          end;
    1.11  
     2.1 --- a/src/HOLCF/ax_ops/thy_ops.ML	Fri Jul 18 13:54:41 1997 +0200
     2.2 +++ b/src/HOLCF/ax_ops/thy_ops.ML	Fri Jul 18 13:55:09 1997 +0200
     2.3 @@ -154,7 +154,7 @@
     2.4    | syn_decls _ _ [] = [];
     2.5  
     2.6  fun translate name vars rhs = 
     2.7 -    Syntax.<-> ((Ast.mk_appl (Constant (mk_internal_name name)) 
     2.8 +    Syntax.ParsePrintRule ((Ast.mk_appl (Constant (mk_internal_name name)) 
     2.9  		 (map Variable vars)), 
    2.10  		rhs); 
    2.11  
    2.12 @@ -178,7 +178,7 @@
    2.13              |   argnames _ _ = [];
    2.14              val names = argnames (ord"A") typ;
    2.15          in if names = [] then [] else 
    2.16 -	    [Syntax.<-> (mk_appl (Constant name) (map Variable names),
    2.17 +	    [Syntax.ParsePrintRule (mk_appl (Constant name) (map Variable names),
    2.18  			 foldl (fn (t,arg) => 
    2.19  				(mk_appl (Constant "@fapp") [t,Variable arg]))
    2.20  			 (Constant name,names))] 
    2.21 @@ -207,7 +207,7 @@
    2.22  	    val vars = map Variable (case typ of (Type("->" ,[t,_])) =>argnames (ord"A") t
    2.23  						 | _ => []);
    2.24          in if vars = [] then [] else 
    2.25 -	    [Syntax.<-> 
    2.26 +	    [Syntax.ParsePrintRule 
    2.27  	     (mk_appl (Constant name) vars,
    2.28  	      mk_appl (Constant "@fapp")
    2.29  	      [Constant name, 
     3.1 --- a/src/HOLCF/domain/syntax.ML	Fri Jul 18 13:54:41 1997 +0200
     3.2 +++ b/src/HOLCF/domain/syntax.ML	Fri Jul 18 13:55:09 1997 +0200
     3.3 @@ -79,13 +79,15 @@
     3.4  	fun arg1 n (con,_,args) = if args = [] then expvar n 
     3.5  				  else mk_appl (Constant "LAM ") 
     3.6  		 [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
     3.7 -  in mk_appl (Constant "@case") [Variable "x", foldr'
     3.8 +  in
     3.9 +    ParsePrintRule
    3.10 +      (mk_appl (Constant "@case") [Variable "x", foldr'
    3.11  				 (fn (c,cs) => mk_appl (Constant "@case2") [c,cs])
    3.12 -				 (mapn case1 1 cons')] <->
    3.13 -     mk_appl (Constant "@fapp") [foldl 
    3.14 +				 (mapn case1 1 cons')],
    3.15 +       mk_appl (Constant "@fapp") [foldl 
    3.16  				 (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
    3.17  				 (Constant (dname^"_when"),mapn arg1 1 cons'),
    3.18 -				 Variable "x"]
    3.19 +				 Variable "x"])
    3.20    end;
    3.21  end;
    3.22