# HG changeset patch
# User wenzelm
# Date 1136557102 -3600
# Node ID 4ce4dba4af0786dfe3f08807d228511dde0eb827
# Parent  451d622bb4a9564d8ecf0120104ec6785ceceed9
Toplevel.theory_to_proof;

diff -r 451d622bb4a9 -r 4ce4dba4af07 src/Pure/Tools/class_package.ML
--- 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];