src/Pure/Isar/proof.ML
changeset 10360 807992b67edd
parent 10350 813a4e8f1276
child 10380 e5370304d893
--- a/src/Pure/Isar/proof.ML	Mon Oct 30 18:25:38 2000 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Oct 30 18:26:14 2000 +0100
@@ -43,7 +43,7 @@
   val pretty_thms: thm list -> Pretty.T
   val verbose: bool ref
   val print_state: int -> state -> unit
-  val pretty_goals: state -> bool -> Pretty.T list
+  val pretty_goals: bool -> state -> Pretty.T list
   val level: state -> int
   type method
   val method: (thm list -> tactic) -> method
@@ -352,9 +352,9 @@
       else pretty_goal (find_goal 0 state))
   in Pretty.writeln (Pretty.chunks prts) end;
 
-fun pretty_goals state print_goal =
+fun pretty_goals main_goal state =
   let val (_, (_, ((_, (_, thm)), _))) = find_goal 0 state
-  in Locale.pretty_sub_goals print_goal (!goals_limit) thm end;
+  in Locale.pretty_sub_goals main_goal (!goals_limit) thm end;