diff -r 22bbc1676768 -r b55686a7b22c src/HOL/IOA/IOA.thy
--- 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 *)