# HG changeset patch
# User blanchet
# Date 1348646459 -7200
# Node ID 7e856b6c5edcd41648e813d45e42e3951c9cc647
# Parent  557302525778ae6a832d84375dd12b88cc07bf99
nicer type var names

diff -r 557302525778 -r 7e856b6c5edc src/HOL/BNF/Tools/bnf_fp_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -46,6 +46,13 @@
     | SOME T' => T')
   | typ_subst inst T = the_default T (AList.lookup (op =) inst T);
 
+fun variant_types ss Ss ctxt =
+  let
+    val (tfrees, _) =
+      fold_map2 (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt);
+    val ctxt' = fold (Variable.declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
+  in (tfrees, ctxt') end;
+
 val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
 
 fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs));
@@ -139,7 +146,7 @@
     val ((Xs, Cs), no_defs_lthy) =
       no_defs_lthy0
       |> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As
-      |> mk_TFrees nn
+      |> variant_types (map (prefix "'") fp_b_names) (replicate nn HOLogic.typeS) |>> map TFree
       ||>> mk_TFrees nn;
 
     (* TODO: cleaner handling of fake contexts, without "background_theory" *)