# HG changeset patch
# User paulson
# Date 846146562 -7200
# Node ID d927beecedf82bc82a9ebec5ae8a7c557f1c7a39
# Parent  92a08ee6a9cb49bccb4782f61cbd61d7bd008216
Allowing negative levels (as offsets) in prlev and choplev

diff -r 92a08ee6a9cb -r d927beecedf8 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Thu Oct 24 10:38:35 1996 +0200
+++ b/src/Pure/goals.ML	Thu Oct 24 10:42:42 1996 +0200
@@ -279,7 +279,9 @@
 (*For inspecting earlier levels of the backward proof*)
 fun chop_level n (pair,pairs) = 
   let val level = length pairs
-  in  if 0<=n andalso n<= level
+  in  if n<0 andalso ~n <= level
+      then  drop (~n, pair::pairs) 
+      else if 0<=n andalso n<= level
       then  drop (level - n, pair::pairs) 
       else  error ("Level number must lie between 0 and " ^ 
 		   string_of_int level)