--- 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;