src/HOL/Tools/Quotient/quotient_typ.ML

--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -45,7 +45,7 @@
   val goals' = map (rpair []) goals
   fun after_qed' thms = after_qed (the_single thms)
 in
-  Proof.theorem_i NONE after_qed' [goals'] ctxt
+  Proof.theorem NONE after_qed' [goals'] ctxt
 end