src/HOLCF/domain/syntax.ML
changeset 15570 8d8c70b41bab
parent 14981 e73f8140af78
child 15574 b1d1b5bfc464
     1.1 --- a/src/HOLCF/domain/syntax.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/HOLCF/domain/syntax.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -22,14 +22,14 @@
     1.4  			    else foldr' mk_sprodT (map opt_lazy args);
     1.5    fun freetvar s = let val tvar = mk_TFree s in
     1.6  		   if tvar mem typevars then freetvar ("t"^s) else tvar end;
     1.7 -  fun when_type (_   ,_,args) = foldr (op ->>) (map third args,freetvar "t");
     1.8 +  fun when_type (_   ,_,args) = Library.foldr (op ->>) (map third args,freetvar "t");
     1.9  in
    1.10    val dtype  = Type(dname,typevars);
    1.11    val dtype2 = foldr' mk_ssumT (map prod cons');
    1.12    val dnam = Sign.base_name dname;
    1.13    val const_rep  = (dnam^"_rep" ,              dtype  ->> dtype2, NoSyn);
    1.14    val const_abs  = (dnam^"_abs" ,              dtype2 ->> dtype , NoSyn);
    1.15 -  val const_when = (dnam^"_when",foldr (op ->>) ((map when_type cons'),
    1.16 +  val const_when = (dnam^"_when",Library.foldr (op ->>) ((map when_type cons'),
    1.17  					        dtype ->> freetvar "t"), NoSyn);
    1.18    val const_copy = (dnam^"_copy", dtypeprod ->> dtype  ->> dtype , NoSyn);
    1.19  end;
    1.20 @@ -42,7 +42,7 @@
    1.21  							 else      c::esc cs
    1.22  	|   esc []      = []
    1.23  	in implode o esc o Symbol.explode end;
    1.24 -  fun con (name,s,args) = (name,foldr (op ->>) (map third args,dtype),s);
    1.25 +  fun con (name,s,args) = (name,Library.foldr (op ->>) (map third args,dtype),s);
    1.26    fun dis (con ,s,_   ) = (dis_name_ con, dtype->>trT,
    1.27  			   Mixfix(escape ("is_" ^ con), [], Syntax.max_pri));
    1.28  			(* stricly speaking, these constants have one argument,
    1.29 @@ -52,7 +52,7 @@
    1.30  in
    1.31    val consts_con = map con cons';
    1.32    val consts_dis = map dis cons';
    1.33 -  val consts_sel = flat(map sel cons');
    1.34 +  val consts_sel = List.concat(map sel cons');
    1.35  end;
    1.36  
    1.37  (* ----- constants concerning induction ------------------------------------- *)
    1.38 @@ -70,7 +70,7 @@
    1.39  					 (string_of_int m));
    1.40  	fun app s (l,r)   = mk_appl (Constant s) [l,r];
    1.41  	fun case1 n (con,mx,args) = mk_appl (Constant "_case1")
    1.42 -		 [foldl (app "Rep_CFun") (c_ast con mx, (mapn (argvar n) 1 args)),
    1.43 +		 [Library.foldl (app "Rep_CFun") (c_ast con mx, (mapn (argvar n) 1 args)),
    1.44  		  expvar n];
    1.45  	fun arg1 n (con,_,args) = if args = [] then expvar n 
    1.46  				  else mk_appl (Constant "LAM ") 
    1.47 @@ -80,7 +80,7 @@
    1.48        (mk_appl (Constant "_case_syntax") [Variable "x", foldr'
    1.49  				(fn (c,cs) => mk_appl (Constant"_case2") [c,cs])
    1.50  				 (mapn case1 1 cons')],
    1.51 -       mk_appl (Constant "Rep_CFun") [foldl 
    1.52 +       mk_appl (Constant "Rep_CFun") [Library.foldl 
    1.53  				(fn (w,a ) => mk_appl (Constant"Rep_CFun" ) [w,a ])
    1.54  				 (Constant (dnam^"_when"),mapn arg1 1 cons'),
    1.55  				 Variable "x"])
    1.56 @@ -107,10 +107,10 @@
    1.57    val const_copy   = (comp_dnam^"_copy"  ,funprod ->> funprod, NoSyn);
    1.58    val const_bisim  = (comp_dnam^"_bisim" ,relprod --> boolT  , NoSyn);
    1.59    val ctt           = map (calc_syntax funprod) eqs';
    1.60 -in thy'' |> ContConsts.add_consts_i (flat (map fst ctt) @ 
    1.61 +in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @ 
    1.62  				    (if length eqs'>1 then [const_copy] else[])@
    1.63  				    [const_bisim])
    1.64 -	 |> Theory.add_trrules_i (flat(map snd ctt))
    1.65 +	 |> Theory.add_trrules_i (List.concat(map snd ctt))
    1.66  end; (* let *)
    1.67  
    1.68  end; (* local *)