src/Pure/proof_general.ML

--- a/src/Pure/proof_general.ML	Sat Jun 17 19:37:47 2006 +0200
+++ b/src/Pure/proof_general.ML	Sat Jun 17 19:37:48 2006 +0200
@@ -124,14 +124,14 @@
   else bg_tag () ^ x ^ end_tag (), real (Symbol.length (Symbol.explode x)));
 
 fun free_or_skolem x =
-  (case try Syntax.dest_skolem x of
+  (case try Term.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 Syntax.dest_skolem x of
+      (case try Term.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)))