# HG changeset patch
# User blanchet
# Date 1393192271 -3600
# Node ID cf6a029b28d8cf6736b25ab8a58b7178dd542807
# Parent  1f9cc432ecd4975505fbb7dcfca109b95629bc41
more precise error message

diff -r 1f9cc432ecd4 -r cf6a029b28d8 src/HOL/BNF_FP_Base.thy
--- a/src/HOL/BNF_FP_Base.thy	Sun Feb 23 22:51:11 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy	Sun Feb 23 22:51:11 2014 +0100
@@ -154,5 +154,5 @@
 ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML"
 ML_file "Tools/BNF/bnf_fp_n2m.ML"
 ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML"
-
+ 
 end
diff -r 1f9cc432ecd4 -r cf6a029b28d8 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Feb 23 22:51:11 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Feb 23 22:51:11 2014 +0100
@@ -273,12 +273,13 @@
     Type (_, Ts) => map (not o member (op =) (deads_of_bnf bnf)) Ts
   | _ => replicate n false);
 
-fun cannot_merge_types () = error "Mutually recursive types must have the same type parameters";
+fun cannot_merge_types fp =
+  error ("Mutually " ^ co_prefix fp ^ "recursive types must have the same type parameters");
 
-fun merge_type_arg T T' = if T = T' then T else cannot_merge_types ();
+fun merge_type_arg fp T T' = if T = T' then T else cannot_merge_types fp;
 
-fun merge_type_args (As, As') =
-  if length As = length As' then map2 merge_type_arg As As' else cannot_merge_types ();
+fun merge_type_args fp (As, As') =
+  if length As = length As' then map2 (merge_type_arg fp) As As' else cannot_merge_types fp;
 
 fun reassoc_conjs thm =
   reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]})
@@ -970,7 +971,7 @@
 
     val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of_spec) specs;
     val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
-    val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
+    val unsorted_As = Library.foldr1 (merge_type_args fp) unsorted_Ass0;
     val num_As = length unsorted_As;
 
     val set_boss = map (map fst o type_args_named_constrained_of_spec) specs;