src/HOL/IOA/meta_theory/Solve.ML

--- a/src/HOL/IOA/meta_theory/Solve.ML	Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/IOA/meta_theory/Solve.ML	Fri Mar 24 12:30:35 1995 +0100
@@ -18,7 +18,7 @@
   by (safe_tac set_cs);
 
   (* give execution of abstract automata *)
-  by (res_inst_tac[("x","<mk_behaviour A (fst ex),%i.f(snd ex i)>")] bexI 1);
+  by (res_inst_tac[("x","(mk_behaviour A (fst ex),%i.f(snd ex i))")] bexI 1);
 
   (* Behaviours coincide *)
   by (asm_simp_tac (SS addsimps [mk_behaviour_def,filter_oseq_idemp])1);