diff -r 780b7a2c50b6 -r 35bb5b013f0e Nominal/nominal_function.ML --- 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 =