# HG changeset patch
# User wenzelm
# Date 1150565868 -7200
# Node ID f552697b2f195b3d2a780a4bfe10e5bcfb4bc60f
# Parent  c23a0e65b285bfd943f07fe090b07c13054444cf
Term.skolem;

diff -r c23a0e65b285 -r f552697b2f19 TFL/casesplit.ML
--- a/TFL/casesplit.ML	Sat Jun 17 19:37:47 2006 +0200
+++ b/TFL/casesplit.ML	Sat Jun 17 19:37:48 2006 +0200
@@ -179,7 +179,7 @@
       val freets = Term.term_frees gt;
       fun getter x =
           let val (n,ty) = Term.dest_Free x in
-            (if vstr = n orelse vstr = Syntax.dest_skolem n
+            (if vstr = n orelse vstr = Term.dest_skolem n
              then SOME (n,ty) else NONE )
             handle Fail _ => NONE (* dest_skolem *)
           end;
diff -r c23a0e65b285 -r f552697b2f19 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)))