# HG changeset patch
# User traytel
# Date 1384353392 -3600
# Node ID edb87aac9cca741fb9b16d43e757b36db2966470
# Parent  adbcad187fcfed8ac75d0ae9e76214985024cbf8
prohibit locally fixed type variables in bnf definitions

diff -r adbcad187fcf -r edb87aac9cca src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Wed Nov 13 15:36:32 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed Nov 13 15:36:32 2013 +0100
@@ -744,8 +744,12 @@
 
     val CA_params = map TVar (Term.add_tvarsT CA []);
 
+    val bnf_T = Morphism.typ phi T_rhs;
+    val bad_args = Term.add_tfreesT bnf_T [];
+    val _ = if null bad_args then () else error ("Locally fixed type arguments " ^
+      commas_quote (map (Syntax.string_of_typ no_defs_lthy o TFree) bad_args));
+
     val bnf_sets = map2 (normalize_set CA_params) alphas (map (Morphism.term phi) bnf_set_terms);
-    val bnf_T = Morphism.typ phi T_rhs;
     val bnf_bd =
       Term.subst_TVars (Term.add_tvar_namesT bnf_T [] ~~ CA_params) (Morphism.term phi bnf_bd_term);