# HG changeset patch
# User blanchet
# Date 1376053419 -7200
# Node ID cdd1d50492873a26c78abbeeca54eb2788e0906a
# Parent  551d09fc245c24b4da18daf36fa19d7e9960c217
honor user type names if possible

diff -r 551d09fc245c -r cdd1d5049287 src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Fri Aug 09 13:57:21 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Fri Aug 09 15:03:39 2013 +0200
@@ -204,7 +204,7 @@
 
     val (As, B) =
       no_defs_lthy
-      |> mk_TFrees' (map Type.sort_of_atyp As0)
+      |> variant_tfrees (map (fst o fst o dest_TVar) As0)
       ||> the_single o fst o mk_TFrees 1;
 
     val dataT = Type (dataT_name, As);
diff -r 551d09fc245c -r cdd1d5049287 src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Fri Aug 09 13:57:21 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Fri Aug 09 15:03:39 2013 +0200
@@ -134,10 +134,6 @@
   val base_name_of_typ: typ -> string
   val mk_common_name: string list -> string
 
-  val variant_types: string list -> sort list -> Proof.context ->
-    (string * sort) list * Proof.context
-  val variant_tfrees: string list -> Proof.context -> typ list * Proof.context
-
   val split_conj_thm: thm -> thm list
   val split_conj_prems: int -> thm -> thm
 
@@ -428,16 +424,6 @@
 (*dangerous; use with monotonic, converging functions only!*)
 fun fixpoint eq f X = if subset eq (f X, X) then X else fixpoint eq f (f X);
 
-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;
-
-fun variant_tfrees ss =
-  apfst (map TFree) o variant_types (map (prefix "'") ss) (replicate (length ss) HOLogic.typeS);
-
 (* stolen from "~~/src/HOL/Tools/Datatype/datatype_aux.ML" *)
 fun split_conj_thm th =
   ((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th];
diff -r 551d09fc245c -r cdd1d5049287 src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Fri Aug 09 13:57:21 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Fri Aug 09 15:03:39 2013 +0200
@@ -68,6 +68,9 @@
   val mk_Freess': string -> typ list list -> Proof.context ->
     (term list list * (string * typ) list list) * Proof.context
   val retype_free: typ -> term -> term
+  val variant_types: string list -> sort list -> Proof.context ->
+    (string * sort) list * Proof.context
+  val variant_tfrees: string list -> Proof.context -> typ list * Proof.context
   val nonzero_string_of_int: int -> string
 
   val num_binder_types: typ -> int
@@ -384,6 +387,19 @@
 fun retype_free T (Free (s, _)) = Free (s, T)
   | retype_free _ t = raise TERM ("retype_free", [t]);
 
+fun ensure_prefix pre s = s |> not (String.isPrefix pre s) ? prefix pre;
+
+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;
+
+fun variant_tfrees ss =
+  apfst (map TFree) o
+    variant_types (map (ensure_prefix "'") ss) (replicate (length ss) HOLogic.typeS);
+
 
 (** Types **)