--- a/Nominal/nominal_termination.ML	Sun Dec 15 15:14:40 2013 +1100
+++ b/Nominal/nominal_termination.ML	Sat Jan 11 23:17:23 2014 +0000
@@ -92,7 +92,7 @@
        [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
     |> Proof_Context.note_thmss ""
        [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
-         [([Goal.norm_result termination], [])])] |> snd
+         [([Goal.norm_result lthy termination], [])])] |> snd
     |> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]]
   end