src/Pure/proofterm.ML
changeset 36732 9c2ee10809b2
parent 36621 2fd4e2c76636
child 36740 6248aa22c694
     1.1 --- a/src/Pure/proofterm.ML	Fri May 07 17:03:06 2010 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Fri May 07 19:50:50 2010 +0200
     1.3 @@ -891,7 +891,7 @@
     1.4  fun strip_shyps_proof algebra present witnessed extra_sorts prf =
     1.5    let
     1.6      fun get S2 (T, S1) = if Sorts.sort_le algebra (S1, S2) then SOME T else NONE;
     1.7 -    val extra = map (fn S => (TFree (Name.aT, S), S)) extra_sorts;
     1.8 +    val extra = map (fn S => (TFree ("'dummy", S), S)) extra_sorts;
     1.9      val replacements = present @ extra @ witnessed;
    1.10      fun replace T =
    1.11        if exists (fn (T', _) => T' = T) present then raise Same.SAME