# HG changeset patch
# User blanchet
# Date 1377793451 -7200
# Node ID de1dc709f9d475444b29006faa25e34d563fc29f
# Parent  89f7f1cc9ae3ac1b8cadebd6b280e72d201c66f7
handle type class annotations on (co)datatype parameters gracefully

diff -r 89f7f1cc9ae3 -r de1dc709f9d4 src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Thu Aug 29 17:57:25 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Thu Aug 29 18:24:11 2013 +0200
@@ -199,15 +199,17 @@
       Binding.qualify mandatory data_b_name o
       (rep_compat ? Binding.qualify false rep_compat_prefix);
 
-    fun tfree_name_of (TFree (s, _)) = s
-      | tfree_name_of (TVar ((s, _), _)) = s
-      | tfree_name_of (Type (s, _)) = Long_Name.base_name s;
+    fun dest_TFree_or_TVar (TFree p) = p
+      | dest_TFree_or_TVar (TVar ((s, _), S)) = (s, S)
+      | dest_TFree_or_TVar _ = error "Invalid type argument";
 
-    val (As, B) =
+    val (unsorted_As, B) =
       no_defs_lthy
-      |> variant_tfrees (map tfree_name_of As0)
+      |> variant_tfrees (map (fst o dest_TFree_or_TVar) As0)
       ||> the_single o fst o mk_TFrees 1;
 
+    val As = map2 (resort_tfree o snd o dest_TFree_or_TVar) As0 unsorted_As;
+
     val dataT = Type (dataT_name, As);
     val ctrs = map (mk_ctr As) ctrs0;
     val ctr_Tss = map (binder_types o fastype_of) ctrs;
diff -r 89f7f1cc9ae3 -r de1dc709f9d4 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 17:57:25 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 18:24:11 2013 +0200
@@ -1055,11 +1055,9 @@
       ||>> mk_TFrees nn
       ||>> variant_tfrees fp_b_names;
 
-    fun add_fake_type spec =
-      Typedecl.basic_typedecl (type_binding_of spec, num_As, mixfix_of spec)
-      #>> (fn s => Type (s, unsorted_As));
+    fun add_fake_type spec = Typedecl.basic_typedecl (type_binding_of spec, num_As, mixfix_of spec);
 
-    val (fake_Ts, fake_lthy) = fold_map add_fake_type specs no_defs_lthy0;
+    val (fake_T_names, fake_lthy) = fold_map add_fake_type specs no_defs_lthy0;
 
     val qsoty = quote o Syntax.string_of_typ fake_lthy;
 
@@ -1100,6 +1098,8 @@
       | extras => error ("Extra type variables on right-hand side: " ^
           commas (map (qsoty o TFree) extras)));
 
+    val fake_Ts = map (fn s => Type (s, As)) fake_T_names;
+
     fun eq_fpT_check (T as Type (s, Ts)) (T' as Type (s', Ts')) =
         s = s' andalso (Ts = Ts' orelse
           error ("Wrong type arguments in " ^ co_prefix fp ^ "recursive type " ^ qsoty T ^
@@ -1279,7 +1279,7 @@
 
             val inject_tacss =
               map2 (fn 0 => K [] | _ => fn ctr_def => [fn {context = ctxt, ...} =>
-                  mk_inject_tac ctxt ctr_def ctor_inject]) ms ctr_defs;
+                mk_inject_tac ctxt ctr_def ctor_inject]) ms ctr_defs;
 
             val half_distinct_tacss =
               map (map (fn (def, def') => fn {context = ctxt, ...} =>