--- a/Nominal/Nominal2_Abs.thy	Mon Apr 01 23:22:53 2013 +0100
+++ b/Nominal/Nominal2_Abs.thy	Fri Apr 19 00:10:52 2013 +0100
@@ -922,9 +922,8 @@
 
 
 ML {*
-fun alpha_single_simproc thm _ ss ctrm =
+fun alpha_single_simproc thm _ ctxt ctrm =
  let
-    val ctxt = Simplifier.the_context ss
     val thy = Proof_Context.theory_of ctxt
     val _ $ (_ $ x) $ (_ $ y) = term_of ctrm
     val cvrs = union (op =) (Term.add_frees x []) (Term.add_frees y [])