--- a/src/Pure/Tools/plugin.ML Wed Dec 17 16:10:30 2014 +0100 +++ b/src/Pure/Tools/plugin.ML Wed Dec 17 16:51:29 2014 +0100 @@ -186,4 +186,3 @@ #> perhaps consolidate'; end; -