src/Pure/Isar/proof.ML
changeset 10320 26d4b84eb047
parent 9482 9c438a65be0a
child 10350 813a4e8f1276
--- 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 **)