src/Pure/Thy/thy_info.ML

 
 
 
 (** thy database **)
 
+(* base name *)
+
+fun base_name s = Path.implode (Path.base (Path.explode s));
+
+
 (* messages *)
 
 fun loader_msg txt [] = "Theory loader: " ^ txt
   | loader_msg txt names = "Theory loader: " ^ txt ^ " " ^ commas_quote names;
 

   imports: string list};  (*source specification of imports (partially qualified)*)
 
 fun make_deps master imports : deps = {master = master, imports = imports};
 
 fun master_dir (d: deps option) = the_default Path.current (Option.map (Path.dir o #1 o #master) d);
-fun base_name s = Path.implode (Path.base (Path.explode s));
 
 local
   val database = Unsynchronized.ref (Graph.empty: (deps option * theory option) Graph.T);
 in
   fun get_thys () = ! database;