# HG changeset patch
# User wenzelm
# Date 1152613026 -7200
# Node ID c9da24b69fdabe1be13241511e0801d809cd5e3f
# Parent  1398063aa271ea317e19c2395a4f37cb9797d696
Name.dest_skolem;

diff -r 1398063aa271 -r c9da24b69fda TFL/casesplit.ML
--- a/TFL/casesplit.ML	Tue Jul 11 12:17:05 2006 +0200
+++ b/TFL/casesplit.ML	Tue Jul 11 12:17:06 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 = Term.dest_skolem n
+            (if vstr = n orelse vstr = Name.dest_skolem n
              then SOME (n,ty) else NONE )
             handle Fail _ => NONE (* dest_skolem *)
           end;
diff -r 1398063aa271 -r c9da24b69fda src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Tue Jul 11 12:17:05 2006 +0200
+++ b/src/Pure/proof_general.ML	Tue Jul 11 12:17:06 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 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)))