--- a/src/HOL/Nominal/nominal_package.ML Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOL/Nominal/nominal_package.ML Thu Mar 20 12:09:20 2008 +0100
@@ -959,7 +959,7 @@
alpha @ abs_perm @ abs_fresh @ rep_inject_thms @
perm_rep_perm_thms)) 1),
TRY (asm_full_simp_tac (HOL_basic_ss addsimps (perm_fun_def ::
- expand_fun_eq :: rep_inject_thms @ perm_rep_perm_thms)) 1)])
+ @{thm expand_fun_eq} :: rep_inject_thms @ perm_rep_perm_thms)) 1)])
end) (constrs ~~ constr_rep_thms)
end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);