src/HOL/ex/svc_funcs.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
     1.1 --- a/src/HOL/ex/svc_funcs.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/HOL/ex/svc_funcs.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -44,11 +44,11 @@
     1.4  
     1.5   fun toString t =
     1.6       let fun ue (Buildin(s, l)) = 
     1.7 -	     "(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
     1.8 +	     "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
     1.9  	   | ue (Interp(s, l)) = 
    1.10 -	     "{" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
    1.11 +	     "{" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
    1.12  	   | ue (UnInterp(s, l)) = 
    1.13 -	     "(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    1.14 +	     "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    1.15  	   | ue (FalseExpr) = "FALSE "
    1.16  	   | ue (TrueExpr)  = "TRUE "
    1.17  	   | ue (Int i)     = (signedInt i) ^ " "
    1.18 @@ -243,7 +243,7 @@
    1.19  
    1.20        val body_e = mt pos body  (*evaluate now to assign into !nat_vars*)
    1.21    in 
    1.22 -     foldr add_nat_var (!nat_vars, body_e) 
    1.23 +     Library.foldr add_nat_var (!nat_vars, body_e) 
    1.24    end;
    1.25  
    1.26