--- a/Nominal/Nominal2_FCB.thy	Mon Apr 01 23:22:53 2013 +0100
+++ b/Nominal/Nominal2_FCB.thy	Fri Apr 19 00:10:52 2013 +0100
@@ -12,7 +12,7 @@
 val all_trivials : (Proof.context -> Method.method) context_parser =
 Scan.succeed (fn ctxt =>
  let
-   val tac = TRYALL (SOLVED' (full_simp_tac (simpset_of ctxt)))
+   val tac = TRYALL (SOLVED' (full_simp_tac ctxt))
  in 
    Method.SIMPLE_METHOD' (K tac)
  end)