reject mapper terms with type variables not contained in the term's type

--- a/src/HOL/Tools/enriched_type.ML	Fri Mar 09 20:17:16 2012 +0100
+++ b/src/HOL/Tools/enriched_type.ML	Fri Mar 09 20:50:28 2012 +0100
@@ -201,9 +201,13 @@
     val input_mapper = prep_term lthy raw_mapper;
     val T = fastype_of input_mapper;
     val _ = Type.no_tvars T;
+    val _ = case subtract (op =) (Term.add_tfreesT T []) (Term.add_tfrees input_mapper [])
+     of [] => ()
+      | vs => error ("Illegal additional type variable(s) in term: "
+          ^ commas (map (Syntax.string_of_typ lthy o TFree) vs));
     val mapper = singleton (Variable.polymorphic lthy) input_mapper;
     val _ = if null (Term.add_tfreesT (fastype_of mapper) []) then ()
-      else error ("Illegal locally fixed variables in type: " ^ Syntax.string_of_typ lthy T);
+      else error ("Illegal locally fixed type variable(s) in type: " ^ Syntax.string_of_typ lthy T);
     fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
       | add_tycos _ = I;
     val tycos = add_tycos T [];