src/HOL/Nominal/nominal_permeq.ML

       rtac (perm_fun_def RS meta_eq_to_obj_eq RS trans) i)
 
 (* applies the ext-rule such that      *)
 (*                                     *)
 (*    f = g   goes to  /\x. f x = g x  *)
-fun ext_fun_tac i = ("extensionality expansion of functions", rtac ext i);
+fun ext_fun_tac i = ("extensionality expansion of functions", rtac @{thm ext} i);
 
 
 (* perm_extend_simp_tac_i is perm_simp plus additional tactics        *)
 (* to decide equation that come from support problems             *)
 (* since it contains looping rules the "recursion" - depth is set *)