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, ...} =>