src/Pure/proof_general.ML

 fun tagit (kind, bg_tag) x =
  (if Output.has_mode pgmlatomsN then xml_atom kind x
   else bg_tag () ^ x ^ end_tag (), real (Symbol.length (Symbol.explode x)));
 
 fun free_or_skolem x =
-  (case try Term.dest_skolem x of
+  (case try Name.dest_skolem x of
     NONE => tagit free_tag x
   | SOME x' => tagit skolem_tag x');
 
 fun var_or_skolem s =
   (case Syntax.read_variable s of
     SOME (x, i) =>
-      (case try Term.dest_skolem x of
+      (case try Name.dest_skolem x of
         NONE => tagit var_tag s
       | SOME x' => tagit skolem_tag
           (setmp show_question_marks true Syntax.string_of_vname (x', i)))
   | NONE => tagit var_tag s);