changeset 43278 | 1fbdcebb364b |
parent 42425 | 2aa907d5ee4f |
child 43761 | e72ba84ae58f |
--- 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' =