src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML

     val (unsorted_As, B) =
       no_defs_lthy
       |> 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 As = map2 (resort_tfree_or_tvar o snd o dest_TFree_or_TVar) As0 unsorted_As;
 
     val fcT = Type (fcT_name, As);
     val ctrs = map (mk_ctr As) ctrs0;
     val ctr_Tss = map (binder_types o fastype_of) ctrs;