--- a/Nominal/nominal_function_core.ML	Wed May 25 21:38:50 2011 +0200
+++ b/Nominal/nominal_function_core.ML	Thu May 26 06:36:29 2011 +0200
@@ -793,7 +793,7 @@
     Goal.init goal
     |> (SINGLE (resolve_tac [accI] 1)) |> the
     |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1))  |> the
-    |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the
+    |> (SINGLE (auto_tac ctxt)) |> the
     |> Goal.conclude
     |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   end