# HG changeset patch
# User wenzelm
# Date 1273254650 -7200
# Node ID 9c2ee10809b2a214c55cd4dec24b7269ee15301f
# Parent  08cd7eccb043754ca6754826fd0a39ffd02ec566
strip_shyps_proof: dummy TFrees are called "'dummy" as in del_conflicting_tvars below;

diff -r 08cd7eccb043 -r 9c2ee10809b2 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri May 07 17:03:06 2010 +0200
+++ b/src/Pure/proofterm.ML	Fri May 07 19:50:50 2010 +0200
@@ -891,7 +891,7 @@
 fun strip_shyps_proof algebra present witnessed extra_sorts prf =
   let
     fun get S2 (T, S1) = if Sorts.sort_le algebra (S1, S2) then SOME T else NONE;
-    val extra = map (fn S => (TFree (Name.aT, S), S)) extra_sorts;
+    val extra = map (fn S => (TFree ("'dummy", S), S)) extra_sorts;
     val replacements = present @ extra @ witnessed;
     fun replace T =
       if exists (fn (T', _) => T' = T) present then raise Same.SAME