src/CTT/ex/Typechecking.thy

--- a/src/CTT/ex/Typechecking.thy	Mon Sep 06 19:11:01 2010 +0200
+++ b/src/CTT/ex/Typechecking.thy	Mon Sep 06 19:13:10 2010 +0200
@@ -66,7 +66,7 @@
 
 (*Proofs involving arbitrary types.
   For concreteness, every type variable left over is forced to be N*)
-ML {* val N_tac = TRYALL (rtac (thm "NF")) *}
+ML {* val N_tac = TRYALL (rtac @{thm NF}) *}
 
 schematic_lemma "lam w. <w,w> : ?A"
 apply (tactic "typechk_tac []")