prove: error with original thread position;
authorwenzelm
Thu Sep 25 14:35:01 2008 +0200 (2008-09-25)
changeset 28355b9d9360e2440
parent 28354 c5fe7372ae4e
child 28356 ac4498f95d1c
prove: error with original thread position;
src/Pure/goal.ML
     1.1 --- a/src/Pure/goal.ML	Thu Sep 25 13:21:13 2008 +0200
     1.2 +++ b/src/Pure/goal.ML	Thu Sep 25 14:35:01 2008 +0200
     1.3 @@ -147,9 +147,11 @@
     1.4      val thy = ProofContext.theory_of ctxt;
     1.5      val string_of_term = Syntax.string_of_term ctxt;
     1.6  
     1.7 +    val pos = Position.thread_data ();
     1.8      fun err msg = cat_error msg
     1.9        ("The error(s) above occurred for the goal statement:\n" ^
    1.10 -        string_of_term (Logic.list_implies (asms, Logic.mk_conjunction_list props)));
    1.11 +        string_of_term (Logic.list_implies (asms, Logic.mk_conjunction_list props)) ^
    1.12 +        (case Position.str_of pos of "" => "" | s => "\n" ^ s));
    1.13  
    1.14      fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm (Term.no_dummy_patterns t))
    1.15        handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;