src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -3059,7 +3059,7 @@
            ) options [const]))
       end
   in
-    Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
+    Proof.theorem NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
   end;
 
 val code_pred = generic_code_pred (K I);