# HG changeset patch
# User wenzelm
# Date 1142435892 -3600
# Node ID b85e16bd70d0e0f24bbc74007bd90c29bbf2e1a5
# Parent  05b6d220e5091df477e3ce0e2ac1c6b39a3b2f13
rename_frees: treat trivial names;
monomorphic: tuned invented names;

diff -r 05b6d220e509 -r b85e16bd70d0 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Mar 14 22:07:33 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Mar 15 16:18:12 2006 +0100
@@ -662,7 +662,7 @@
     val (types, sorts, _, _) = defaults_of (ctxt |> fold declare_syntax ts);
     fun rename (x, X) xs =
       let
-        fun used y = member (op =) xs y orelse
+        fun used y = y = "" orelse y = "'" orelse member (op =) xs y orelse
           Vartab.defined types (y, ~1) orelse Vartab.defined sorts (y, ~1);
         val x' = Term.variant_name used x;
       in ((x', X), x' :: xs) end;
@@ -725,7 +725,7 @@
 fun monomorphic ctxt ts =
   let
     val tvars = fold Term.add_tvars ts [];
-    val tfrees = map TFree (rename_frees ctxt ts (map (apfst fst) tvars));
+    val tfrees = map TFree (rename_frees ctxt ts (map (pair "'" o #2) tvars));
     val specialize = Term.instantiate ((tvars ~~ tfrees), []);
   in map specialize ts end;