diff -r a9685909944d -r e4d8dfb7e34a CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Tue Feb 24 22:23:07 2009 +0000 +++ b/CookBook/FirstSteps.thy Wed Feb 25 10:09:18 2009 +0000 @@ -842,14 +842,13 @@ @{ML_response_fake [display,gray] "let - val thy = @{theory} - val assm1 = cterm_of thy @{prop \"\(x::nat). P x \ Q x\"} - val assm2 = cterm_of thy @{prop \"(P::nat\bool) t\"} + val assm1 = @{cprop \"\(x::nat). P x \ Q x\"} + val assm2 = @{cprop \"(P::nat\bool) t\"} val Pt_implies_Qt = assume assm1 - |> forall_elim (cterm_of thy @{term \"t::nat\"}); + |> forall_elim @{cterm \"t::nat\"}; val Qt = implies_elim Pt_implies_Qt (assume assm2); in