--- a/src/Pure/Tools/invoke.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Pure/Tools/invoke.ML Sat Oct 06 16:50:04 2007 +0200
@@ -115,7 +115,7 @@
local structure P = OuterParse and K = OuterKeyword in
-val invokeP =
+val _ =
OuterSyntax.command "invoke"
"schematic invocation of locale expression in proof context"
(K.tag_proof K.prf_goal)
@@ -123,8 +123,6 @@
>> (fn (((name, expr), (insts, _)), fixes) =>
Toplevel.print o Toplevel.proof' (invoke name expr insts fixes)));
-val _ = OuterSyntax.add_parsers [invokeP];
-
end;
end;