author | urbanc |
Thu, 22 Mar 2007 11:17:32 +0100 | |
changeset 22495 | c54748fd1f43 |
parent 22494 | b61306c7987a |
child 22496 | 1f428200fd9c |
--- a/src/HOL/Nominal/nominal_thmdecls.ML Thu Mar 22 10:35:12 2007 +0100 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Thu Mar 22 11:17:32 2007 +0100 @@ -139,7 +139,8 @@ in if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name])) then [(pi,typi)] - else raise EQVT_FORM "Could not find a permutation" + else raise + EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name) end | Abs (_,_,t1) => get_pi_aux t1 | (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2