--- a/Nominal/nominal_function.ML	Sun Dec 15 15:14:40 2013 +1100
+++ b/Nominal/nominal_function.ML	Sat Jan 11 23:17:23 2014 +0000
@@ -216,7 +216,7 @@
   in
     lthy'
     |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]]
-    |> Proof.refine (Method.primitive_text (K goal_state)) |> Seq.hd
+    |> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd
   end
 
 val nominal_function =