src/HOLCF/IOA/meta_theory/CompoTraces.ML

 (* both sides of this equation are UU *)
 by (subgoal_tac "schA=UU" 1);
 by (Asm_simp_tac 1);
 (* first side: mksch = UU *)
 by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU,
-                                           (finiteR_mksch RS mp COMP rev_contrapos),
-                                            ForallBnAmksch],
-                           simpset())) 1);
+        (finiteR_mksch RS mp COMP rev_contrapos),ForallBnAmksch],simpset())) 1);
 (* schA = UU *)
 by (eres_inst_tac [("A","A")] LastActExtimplUU 1);
 by (Asm_simp_tac 1);
 by (eres_inst_tac [("Q","%x. x:act B & x~:act A")] ForallQFilterPUU 1);
 by (assume_tac 1);