# HG changeset patch
# User haftmann
# Date 1138605531 -3600
# Node ID 4ed69fe8f8870cead9cccaa354b432ae581e7994
# Parent  5fac129ae936e4cd5bb028b608502389f08b2687
moved instance Isar command to class_package.ML

diff -r 5fac129ae936 -r 4ed69fe8f887 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Mon Jan 30 08:17:04 2006 +0100
+++ b/src/Pure/axclass.ML	Mon Jan 30 08:18:51 2006 +0100
@@ -354,13 +354,7 @@
         P.!!! (P.list1 P.xname)) []) -- Scan.repeat P.spec_name
       >> (Toplevel.theory o (snd oo uncurry add_axclass)));
 
-val instanceP =
-  OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
-   ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> instance_subclass ||
-      P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> (instance_arity I o P.triple2))
-    >> (Toplevel.print oo Toplevel.theory_to_proof));
-
-val _ = OuterSyntax.add_parsers [axclassP, instanceP];
+val _ = OuterSyntax.add_parsers [axclassP];
 
 end;