src/Pure/goal.ML
changeset 48992 0518bf89c777
parent 47415 c486ac962b89
child 49009 15381ea111ec
--- 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;