diff -r 0deff0197496 -r 4de3a0d3ae28 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Wed Jan 03 21:23:50 2001 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Wed Jan 03 21:24:29 2001 +0100
@@ -29,20 +29,17 @@
       else if b s then while_aux (b, c, c s)
       else s)"
 
+recdef_tc while_aux_tc: while_aux
+  apply (rule wf_same_fst)
+  apply (rule wf_same_fst)
+  apply (simp add: wf_iff_no_infinite_down_chain)
+  apply blast
+  done
+
 constdefs
   while :: "('a => bool) => ('a => 'a) => 'a => 'a"
   "while b c s == while_aux (b, c, s)"
 
-ML_setup {*
-  goalw_cterm [] (cterm_of (sign_of (the_context ()))
-    (HOLogic.mk_Trueprop (hd (RecdefPackage.tcs_of (the_context ()) "while_aux"))));
-  br wf_same_fst 1;
-  br wf_same_fst 1;
-  by (asm_full_simp_tac (simpset() addsimps [wf_iff_no_infinite_down_chain]) 1);
-  by (Blast_tac 1);
-  qed "while_aux_tc";
-*} (* FIXME cannot access recdef tcs in Isar yet! *)
-
 lemma while_aux_unfold:
   "while_aux (b, c, s) =
     (if \<exists>f. f 0 = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1))