--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Sep 03 20:39:38 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Sep 03 21:13:53 2010 +0200
@@ -97,7 +97,7 @@
if (nprems_of st <= i) then Seq.single st
else raise Fail ("assert_tac: Numbers of subgoals mismatch at goal state :"
^ "\n" ^ Pretty.string_of (Pretty.chunks
- (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st)));
+ (Goal_Display.pretty_goals_without_context st)));
(** fundamentals **)