--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Apr 12 14:54:14 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Apr 12 15:30:38 2013 +0200
@@ -478,7 +478,7 @@
(* It is normally sufficient to apply "assume_tac" to unify the conclusion with
one of the premises. Unfortunately, this sometimes yields "Variable
- ?SK_a_b_c_x has two distinct types" errors. To avoid this, we instantiate the
+ has two distinct types" errors. To avoid this, we instantiate the
variables before applying "assume_tac". Typical constraints are of the form
?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x,
where the nonvariables are goal parameters. *)