--- a/src/HOL/ex/svc_funcs.ML Thu Mar 03 09:22:35 2005 +0100
+++ b/src/HOL/ex/svc_funcs.ML Thu Mar 03 12:43:01 2005 +0100
@@ -44,11 +44,11 @@
fun toString t =
let fun ue (Buildin(s, l)) =
- "(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
+ "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
| ue (Interp(s, l)) =
- "{" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
+ "{" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
| ue (UnInterp(s, l)) =
- "(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
+ "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
| ue (FalseExpr) = "FALSE "
| ue (TrueExpr) = "TRUE "
| ue (Int i) = (signedInt i) ^ " "
@@ -243,7 +243,7 @@
val body_e = mt pos body (*evaluate now to assign into !nat_vars*)
in
- foldr add_nat_var (!nat_vars, body_e)
+ Library.foldr add_nat_var (!nat_vars, body_e)
end;