src/HOL/HOLCF/Universal.thy

--- a/src/HOL/HOLCF/Universal.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/HOLCF/Universal.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -111,12 +111,11 @@
   "ubasis_until P 0 = 0"
 | "finite S \<Longrightarrow> ubasis_until P (node i a S) =
     (if P (node i a S) then node i a S else ubasis_until P a)"
-    apply clarify
-    apply (rule_tac x=b in node_cases)
-     apply simp
+   apply clarify
+   apply (rule_tac x=b in node_cases)
     apply simp
-    apply fast
    apply simp
+   apply fast
   apply simp
  apply simp
 done