# HG changeset patch
# User haftmann
# Date 1331322628 -3600
# Node ID c6235baf20e0704a9f3814345e364eeba6b4e93d
# Parent  7b04cfc24eb666c1e8e66508b35e9746e805e683
reject mapper terms with type variables not contained in the term's type

diff -r 7b04cfc24eb6 -r c6235baf20e0 src/HOL/Tools/enriched_type.ML
--- 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 [];