# HG changeset patch
# User wenzelm
# Date 1184879928 -7200
# Node ID 8f3099589cfabc4f3dfadc867934ec32945a0650
# Parent  b1861768d8f45fceddea2cdd741d154e494d8723
tuned signature;

diff -r b1861768d8f4 -r 8f3099589cfa src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Thu Jul 19 23:18:46 2007 +0200
+++ b/src/Pure/General/path.ML	Thu Jul 19 23:18:48 2007 +0200
@@ -2,14 +2,12 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Abstract algebra of file paths (external encoding Unix-style).
+Abstract algebra of file paths (external encoding in Unix style).
 *)
 
 signature PATH =
 sig
-  datatype elem = Root | Parent | Basic of string | Variable of string
   eqtype T
-  val rep: T -> elem list
   val is_current: T -> bool
   val current: T
   val root: T
diff -r b1861768d8f4 -r 8f3099589cfa src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Thu Jul 19 23:18:46 2007 +0200
+++ b/src/Pure/Thy/thy_header.ML	Thu Jul 19 23:18:48 2007 +0200
@@ -9,8 +9,7 @@
 sig
   val args: OuterLex.token list ->
     (string * string list * (string * bool) list) * OuterLex.token list
-  val read: (string, 'a) Source.source * Position.T ->
-    string * string list * (string * bool) list
+  val read: Position.T -> (string, 'a) Source.source -> string * string list * (string * bool) list
 end;
 
 structure ThyHeader: THY_HEADER =
@@ -49,7 +48,7 @@
     (P.$$$ theoryN -- P.tags) |-- args)) ||
   (P.$$$ theoryN -- P.tags) |-- P.!!! args;
 
-fun read (src, pos) =
+fun read pos src =
   let val res =
     src
     |> Symbol.source false
diff -r b1861768d8f4 -r 8f3099589cfa src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Jul 19 23:18:46 2007 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu Jul 19 23:18:48 2007 +0200
@@ -21,7 +21,7 @@
   datatype markup = Markup | MarkupEnv | Verbatim
   val modes: string list ref
   val eval_antiquote: Scan.lexicon -> Toplevel.node option -> string * Position.T -> string
-  val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
+  val process_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
     Toplevel.transition list -> (OuterLex.token, 'a) Source.source -> Buffer.T
   val output_list: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
     Proof.context -> 'a list -> string
@@ -286,7 +286,7 @@
 end;
 
 
-(* present_thy *)
+(* process_thy *)
 
 datatype markup = Markup | MarkupEnv | Verbatim;
 
@@ -317,7 +317,7 @@
 
 in
 
-fun present_thy lex default_tags is_markup trs src =
+fun process_thy lex default_tags is_markup trs src =
   let
     (* tokens *)