TFL/casesplit.ML

       val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1);
 
       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;
       val (n,ty) = case Library.get_first getter freets
                 of SOME (n, ty) => (n, ty)