--- a/src/Pure/subgoal.ML Thu Jul 30 11:23:57 2009 +0200
+++ b/src/Pure/subgoal.ML Thu Jul 30 12:20:43 2009 +0200
@@ -133,8 +133,5 @@
end;
-val FOCUS_PARAMS = Subgoal.FOCUS_PARAMS;
-val FOCUS_PREMS = Subgoal.FOCUS_PREMS;
-val FOCUS = Subgoal.FOCUS;
val SUBPROOF = Subgoal.SUBPROOF;