# HG changeset patch
# User blanchet
# Date 1396957647 -7200
# Node ID 0c98c911840761ebf7514bbf11a9ff0ee8517239
# Parent  856492b0f755cbea1b4fe37824dbd73f7eeb1bee
preserve user type variable names to avoid mismatches/confusion

diff -r 856492b0f755 -r 0c98c9118407 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Tue Apr 08 12:46:38 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Tue Apr 08 13:47:27 2014 +0200
@@ -47,8 +47,8 @@
 
     val _ = eq_set (op =) (fpT_names, fpT_names') orelse not_mutually_recursive fpT_names;
 
-    val (unsorted_As, _) = lthy |> mk_TFrees (length var_As);
-    val As = map2 (resort_tfree o Type.sort_of_atyp) var_As unsorted_As;
+    val (As_names, _) = lthy |> Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As);
+    val As = map2 (fn s => fn TVar (_, S) => TFree (s, S)) As_names var_As;
     val fpTs as fpT1 :: _ = map (fn s => Type (s, As)) fpT_names';
 
     fun nested_Tparentss_indicessss_of parent_Tkks (T as Type (s, _)) kk =