src/HOL/Nominal/nominal_inductive2.ML

--- a/src/HOL/Nominal/nominal_inductive2.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -445,7 +445,7 @@
 
   in
     ctxt'' |>
-    Proof.theorem_i NONE (fn thss => fn ctxt =>
+    Proof.theorem NONE (fn thss => fn ctxt =>
       let
         val rec_name = space_implode "_" (map Long_Name.base_name names);
         val rec_qualified = Binding.qualify false rec_name;