# HG changeset patch
# User wenzelm
# Date 1491680104 -7200
# Node ID 1f5821b1974153e30878eaa857152cd0e16076ae
# Parent  dccbfc715904a8ebbd7c3a9799f48060c8a2229a
tuned signature;

diff -r dccbfc715904 -r 1f5821b19741 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Apr 08 21:28:19 2017 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sat Apr 08 21:35:04 2017 +0200
@@ -18,8 +18,7 @@
      symbols: HTML.symbols,
      last_timing: Toplevel.transition -> Time.time,
      master_dir: Path.T} -> (string * Position.T) list -> unit
-  val use_thys: (string * Position.T) list -> unit
-  val use_thy: string * Position.T -> unit
+  val use_thy: string -> unit
   val script_thy: Position.T -> string -> theory -> theory
   val register_thy: theory -> unit
   val finish: unit -> unit
@@ -341,18 +340,17 @@
 end;
 
 
-(* use_thy *)
+(* use theories *)
 
 fun use_theories {document, symbols, last_timing, master_dir} imports =
   schedule_tasks
     (snd (require_thys document symbols last_timing [] master_dir imports String_Graph.empty));
 
-val use_thys =
+fun use_thy name =
   use_theories
     {document = false, symbols = HTML.no_symbols, last_timing = K Time.zeroTime,
-      master_dir = Path.current};
-
-val use_thy = use_thys o single;
+      master_dir = Path.current}
+    [(name, Position.none)];
 
 
 (* toplevel scripting -- without maintaining database *)
@@ -389,4 +387,4 @@
 
 end;
 
-fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy (name, Position.none));
+fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy name);