Toplevel.theory_to_proof;

--- a/src/Pure/Tools/class_package.ML	Fri Jan 06 15:18:21 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Fri Jan 06 15:18:22 2006 +0100
@@ -423,7 +423,7 @@
   OuterSyntax.command instanceK "" K.thy_goal
     (P.xname -- (P.$$$ "::" |-- P.!!! P.arity)
       -- Scan.repeat1 P.spec_name
-      >> (Toplevel.theory_theory_to_proof
+      >> (Toplevel.theory_to_proof
           o (fn ((tyco, (asorts, sort)), defs) => add_instance_arity ((tyco, asorts), sort) defs)));
 
 val _ = OuterSyntax.add_parsers [classP, instanceP];