src/HOL/Nominal/nominal_primrec.ML

--- a/src/HOL/Nominal/nominal_primrec.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -363,7 +363,7 @@
   in
     lthy' |>
     Variable.add_fixes (map fst lsrs) |> snd |>
-    Proof.theorem_i NONE
+    Proof.theorem NONE
       (fn thss => fn goal_ctxt =>
          let
            val simps = ProofContext.export goal_ctxt lthy' (flat thss);