src/Pure/thm.ML

--- a/src/Pure/thm.ML	Wed Jun 08 15:39:55 2011 +0200
+++ b/src/Pure/thm.ML	Wed Jun 08 15:56:57 2011 +0200
@@ -1423,7 +1423,7 @@
     and concl = Logic.strip_imp_concl prop;
     val moved_prems = List.drop (prems, j)
     and fixed_prems = List.take (prems, j)
-      handle Subscript => raise THM ("permute_prems: j", j, [rl]);
+      handle General.Subscript => raise THM ("permute_prems: j", j, [rl]);
     val n_j = length moved_prems;
     val m = if k < 0 then n_j + k else k;
     val prop' =