--- a/src/HOL/IOA/IOA.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/IOA/IOA.thy Fri Oct 10 19:02:28 1997 +0200
@@ -104,13 +104,13 @@
(* Restrict the trace to those members of the set s *)
filter_oseq_def
"filter_oseq p s ==
- (%i.case s(i)
+ (%i. case s(i)
of None => None
| Some(x) => if p x then Some x else None)"
mk_trace_def
- "mk_trace(ioa) == filter_oseq(%a.a:externals(asig_of(ioa)))"
+ "mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))"
(* Does an ioa have an execution with the given trace *)