--- a/Nominal/nominal_function.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_function.ML	Sat Mar 19 21:06:48 2016 +0000
@@ -151,7 +151,7 @@
       let
         val NominalFunctionResult {fs, R, psimps, simple_pinducts,
           termination, domintros, cases, eqvts, ...} =
-          cont (Thm.close_derivation proof)
+          cont lthy (Thm.close_derivation proof)
   
         val fnames = map (fst o fst) fixes
         fun qualify n = Binding.name n
@@ -214,7 +214,7 @@
   in
     lthy'
     |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (Thm.concl_of goal_state), [])]]
-    |> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd
+    |> Proof.refine_singleton (Method.primitive_text (K (K goal_state)))
   end
 
 val nominal_function =