# HG changeset patch
# User wenzelm
# Date 881239843 -3600
# Node ID fbb275398eb7d475f730690b31d70ff6f5e55369
# Parent  ab73573067d6af3a559f113aff21b6b8dd251613
added is_base;

diff -r ab73573067d6 -r fbb275398eb7 src/Pure/Thy/path.ML
--- a/src/Pure/Thy/path.ML	Thu Dec 04 13:50:18 1997 +0100
+++ b/src/Pure/Thy/path.ML	Thu Dec 04 13:50:43 1997 +0100
@@ -20,6 +20,7 @@
   val evaluate: (string -> T) -> T -> T
   val expand: (string -> string) -> string -> string
   val base_name: string -> string
+  val is_base: string -> bool
 end;
 
 structure Path: PATH =
@@ -96,5 +97,8 @@
 
 val base_name = base o unpack;
 
+fun is_base str =
+  not (exists (equal "/" orf equal "$") (explode str));
+
 
 end;