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