--- a/src/Pure/Isar/proof.ML Tue Oct 24 23:34:08 2000 +0200
+++ b/src/Pure/Isar/proof.ML Tue Oct 24 23:35:29 2000 +0200
@@ -43,6 +43,7 @@
val pretty_thms: thm list -> Pretty.T
val verbose: bool ref
val print_state: int -> state -> unit
+ val pretty_goals: state -> Pretty.T list
val level: state -> int
type method
val method: (thm list -> tactic) -> method
@@ -351,6 +352,10 @@
else pretty_goal (find_goal 0 state))
in Pretty.writeln (Pretty.chunks prts) end;
+fun pretty_goals state =
+ let val (_, (_, ((_, (_, thm)), _))) = find_goal 0 state
+ in Locale.pretty_goals (! goals_limit) thm end;
+
(** proof steps **)