src/Pure/display.ML
changeset 21646 c07b5b0e8492
parent 20629 8f6cc81ba4a3
child 21721 908a93216f00
     1.1 --- a/src/Pure/display.ML	Tue Dec 05 00:29:19 2006 +0100
     1.2 +++ b/src/Pure/display.ML	Tue Dec 05 00:30:38 2006 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4      val th = Thm.strip_shyps raw_th;
     1.5      val {hyps, tpairs, prop, der = (ora, _), ...} = Thm.rep_thm th;
     1.6      val xshyps = Thm.extra_shyps th;
     1.7 -    val (_, tags) = Thm.get_name_tags th;
     1.8 +    val tags = Thm.get_tags th;
     1.9  
    1.10      val q = if quote then Pretty.quote else I;
    1.11      val prt_term = q o (Pretty.term pp);