diff -r d6a508c16908 -r 6d437bde2f1d src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 20 12:09:20 2008 +0100
@@ -110,7 +110,7 @@
 fun inst_conj_all_tac k = EVERY
   [TRY (EVERY [etac conjE 1, rtac conjI 1, atac 1]),
    REPEAT_DETERM_N k (etac allE 1),
-   simp_tac (HOL_basic_ss addsimps [id_apply]) 1];
+   simp_tac (HOL_basic_ss addsimps [@{thm id_apply}]) 1];
 
 fun map_term f t u = (case f t u of
       NONE => map_term' f t u | x => x)
@@ -305,7 +305,7 @@
           (fn _ => EVERY
             [etac exE 1,
              full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
-             full_simp_tac (HOL_basic_ss addsimps [id_apply]) 1,
+             full_simp_tac (HOL_basic_ss addsimps [@{thm id_apply}]) 1,
              REPEAT (etac conjE 1)])
           [ex] ctxt
       in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
@@ -347,7 +347,7 @@
                     map (fold_rev (NominalPackage.mk_perm [])
                       (rev pis' @ pis)) params' @ [z])) ihyp;
                  fun mk_pi th =
-                   Simplifier.simplify (HOL_basic_ss addsimps [id_apply]
+                   Simplifier.simplify (HOL_basic_ss addsimps [@{thm id_apply}]
                        addsimprocs [NominalPackage.perm_simproc])
                      (Simplifier.simplify eqvt_ss
                        (fold_rev (mk_perm_bool o cterm_of thy)