use RecdefPackage.tcs_of;
authorwenzelm
Thu Oct 19 01:48:26 2000 +0200 (2000-10-19)
changeset 10269cc20c9d7e682
parent 10268 ca52783f9801
child 10270 6086be03a80b
use RecdefPackage.tcs_of;
src/HOL/Library/While_Combinator.thy
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Thu Oct 19 01:47:50 2000 +0200
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Thu Oct 19 01:48:26 2000 +0200
     1.3 @@ -35,13 +35,13 @@
     1.4  
     1.5  ML_setup {*
     1.6    goalw_cterm [] (cterm_of (sign_of (the_context ()))
     1.7 -    (HOLogic.mk_Trueprop (hd while_aux.tcs)));
     1.8 +    (HOLogic.mk_Trueprop (hd (RecdefPackage.tcs_of (the_context ()) "while_aux"))));
     1.9    br wf_same_fstI 1;
    1.10    br wf_same_fstI 1;
    1.11    by (asm_full_simp_tac (simpset() addsimps [wf_iff_no_infinite_down_chain]) 1);
    1.12    by (Blast_tac 1);
    1.13    qed "while_aux_tc";
    1.14 -*} (* FIXME cannot prove recdef tcs in Isar yet! *)
    1.15 +*} (* FIXME cannot access recdef tcs in Isar yet! *)
    1.16  
    1.17  lemma while_aux_unfold:
    1.18    "while_aux (b, c, s) =