clarified error;
authorwenzelm
Sat Jul 25 21:54:09 2015 +0200 (2015-07-25)
changeset 60779c4d3da84d884
parent 60778 682c0dd89b26
child 60780 7e2c8a63a8f8
clarified error;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Sat Jul 25 21:37:09 2015 +0200
     1.2 +++ b/src/Pure/drule.ML	Sat Jul 25 21:54:09 2015 +0200
     1.3 @@ -769,14 +769,13 @@
     1.4                    val t = Var (xi, T);
     1.5                    val u = Thm.term_of cu;
     1.6                  in
     1.7 -                  raise TYPE ("Ill-typed instantiation:\nType\n" ^
     1.8 -                    Syntax.string_of_typ ctxt (Envir.norm_type tyenv T) ^
     1.9 -                    "\nof variable " ^
    1.10 +                  raise THM ("infer_instantiate: type " ^
    1.11 +                    Syntax.string_of_typ ctxt (Envir.norm_type tyenv T) ^ " of variable " ^
    1.12                      Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) t) ^
    1.13 -                    "\ncannot be unified with type\n" ^
    1.14 -                    Syntax.string_of_typ ctxt (Envir.norm_type tyenv U) ^ "\nof term " ^
    1.15 +                    "\ncannot be unified with type " ^
    1.16 +                    Syntax.string_of_typ ctxt (Envir.norm_type tyenv U) ^ " of term " ^
    1.17                      Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) u),
    1.18 -                    [T, U], [t, u])
    1.19 +                    0, [th])
    1.20                  end;
    1.21            in (((xi, T), cu), (tyenv', maxidx')) end;
    1.22