--- a/thys2/UF_Rec.thy	Wed Jun 26 14:42:42 2013 +0100
+++ b/thys2/UF_Rec.thy	Wed Jul 17 10:33:19 2013 +0100
@@ -431,14 +431,8 @@
 apply(simp only: misc if_True)
 apply(simp only: left_std[symmetric] right_std[symmetric])
 apply(simp)
-apply(auto)
-apply(rule_tac x="ka - 1" in exI)
-apply(rule_tac x="l" in exI)
-apply(simp)
-apply (metis Suc_diff_le diff_Suc_Suc diff_zero replicate_Suc)
-apply(rule_tac x="n + 1" in exI)
-apply(simp)
-done
+by (metis Suc_le_D Suc_neq_Zero append_Cons nat.exhaust not_less_eq_eq replicate_Suc)
+
 
 lemma UF_simulate:
   assumes "tm_wf tm"
@@ -665,6 +659,6 @@
   "rec_eval rec_uf [m, cf] = UF m cf"
 by (simp add: rec_uf_def)
 
-
+value "size rec_uf"
 end