src/Provers/order.ML
changeset 43278 1fbdcebb364b
parent 42364 8c674b3b8e44
child 58839 ccda99401bc8
--- a/src/Provers/order.ML	Wed Jun 08 15:39:55 2011 +0200
+++ b/src/Provers/order.ML	Wed Jun 08 15:56:57 2011 +0200
@@ -1247,9 +1247,9 @@
   end
   handle Contr p =>
       (Subgoal.FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st
-        handle Subscript => Seq.empty)
+        handle General.Subscript => Seq.empty)
    | Cannot => Seq.empty
-   | Subscript => Seq.empty)
+   | General.Subscript => Seq.empty)
 end;
 
 (* partial_tac - solves partial orders *)