# HG changeset patch
# User blanchet
# Date 1376256959 -7200
# Node ID 8d581fd1b46f0b4efe606f11484cdc3fb4b788a9
# Parent  5a77edcdbe5436999fc7ea71b68f61f4c67caca4
gracefully fail to define polymorphic (co)datatypes in local context

diff -r 5a77edcdbe54 -r 8d581fd1b46f src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Sun Aug 11 23:35:59 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Sun Aug 11 23:35:59 2013 +0200
@@ -1000,6 +1000,14 @@
     val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
     val set_bss = map (map fst o type_args_named_constrained_of) specs;
 
+    val bad_args =
+      map (Logic.type_map (singleton (Variable.polymorphic no_defs_lthy0))) unsorted_As
+      |> filter_out Term.is_TVar;
+    val _ = null bad_args orelse
+      error ("Locally fixed type argument " ^
+        quote (Syntax.string_of_typ no_defs_lthy0 (hd bad_args)) ^ " in " ^ co_prefix fp ^
+        "datatype specification");
+
     val (((Bs0, Cs), Xs), no_defs_lthy) =
       no_defs_lthy0
       |> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As