src/Pure/proof_general.ML
changeset 20081 c9da24b69fda
parent 19907 f552697b2f19
child 20299 5330f710b960
     1.1 --- a/src/Pure/proof_general.ML	Tue Jul 11 12:17:05 2006 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Tue Jul 11 12:17:06 2006 +0200
     1.3 @@ -124,14 +124,14 @@
     1.4    else bg_tag () ^ x ^ end_tag (), real (Symbol.length (Symbol.explode x)));
     1.5  
     1.6  fun free_or_skolem x =
     1.7 -  (case try Term.dest_skolem x of
     1.8 +  (case try Name.dest_skolem x of
     1.9      NONE => tagit free_tag x
    1.10    | SOME x' => tagit skolem_tag x');
    1.11  
    1.12  fun var_or_skolem s =
    1.13    (case Syntax.read_variable s of
    1.14      SOME (x, i) =>
    1.15 -      (case try Term.dest_skolem x of
    1.16 +      (case try Name.dest_skolem x of
    1.17          NONE => tagit var_tag s
    1.18        | SOME x' => tagit skolem_tag
    1.19            (setmp show_question_marks true Syntax.string_of_vname (x', i)))