--- a/Nominal/nominal_permeq.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_permeq.ML	Sat Mar 19 21:06:48 2016 +0000
@@ -141,7 +141,7 @@
         val ty_insts = map SOME [b, a]
         val term_insts = map SOME [p, f, x]                        
       in
-        Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
+        Thm.instantiate' ty_insts term_insts @{thm eqvt_apply}
       end
   | _ => Conv.no_conv ctrm