# HG changeset patch
# User paulson
# Date 853495998 -3600
# Node ID ea8881e70f9c2153837fe7cd615e536469b179fa
# Parent  d708d8cdc8e8a1de0493a4f5cbd18ec5f60710df
Added the prlim command

diff -r d708d8cdc8e8 -r ea8881e70f9c src/Pure/goals.ML
--- a/src/Pure/goals.ML	Fri Jan 17 11:09:19 1997 +0100
+++ b/src/Pure/goals.ML	Fri Jan 17 11:13:18 1997 +0100
@@ -42,6 +42,7 @@
   val goalw_cterm	: thm list -> cterm -> thm list
   val pop_proof		: unit -> thm list
   val pr		: unit -> unit
+  val prlim		: int -> unit
   val pr_latex		: unit -> unit
   val printgoal_latex	: int -> unit
   val premises		: unit -> thm list
@@ -287,10 +288,13 @@
 		   string_of_int level)
   end;
 
-(*Print the given level of the proof*)
+(*Print the given level of the proof; prlev ~1 prints previous level*)
 fun prlev n = apply_fun (print_top o pop o (chop_level n));
 fun pr () = apply_fun print_top;
 
+(*Set goals_limit and print again*)
+fun prlim n = (goals_limit:=n; pr());
+
 (** the goal.... commands
     Read main goal.  Set global variables curr_prems, curr_mkresult. 
     Initial subgoal and premises are rewritten using rths. **)