--- a/src/Pure/goal.ML Wed Aug 29 11:31:07 2012 +0200
+++ b/src/Pure/goal.ML Wed Aug 29 11:48:45 2012 +0200
@@ -208,7 +208,7 @@
fun err msg = cat_error msg
("The error(s) above occurred for the goal statement:\n" ^
string_of_term (Logic.list_implies (asms, Logic.mk_conjunction_list props)) ^
- (case Position.str_of pos of "" => "" | s => "\n" ^ s));
+ (case Position.here pos of "" => "" | s => "\n" ^ s));
fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm (Term.no_dummy_patterns t))
handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;