# HG changeset patch
# User huffman
# Date 1290897294 28800
# Node ID 6c12f5e24e344c27b95fc99ef43a7d17ce0e8484
# Parent  c8b52f9e16805df9581a1625d7053d2454a43449# Parent  77a468590560f188014148b2e12384ae3738548c
merged

diff -r c8b52f9e1680 -r 6c12f5e24e34 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Sat Nov 27 14:09:03 2010 -0800
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Sat Nov 27 14:34:54 2010 -0800
@@ -983,7 +983,7 @@
     let
       val dir = getenv "ISABELLE_TMP"
       val _ = if !created_temp_dir then ()
-              else (created_temp_dir := true; File.mkdir (Path.explode dir))
+              else (created_temp_dir := true; Isabelle_System.mkdirs (Path.explode dir))
     in (serial_string (), dir) end
 
 (* The fudge term below is to account for Kodkodi's slow start-up time, which
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/HOL/ex/Eval_Examples.thy
--- a/src/HOL/ex/Eval_Examples.thy	Sat Nov 27 14:09:03 2010 -0800
+++ b/src/HOL/ex/Eval_Examples.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -9,26 +9,26 @@
 text {* evaluation oracle *}
 
 lemma "True \<or> False" by eval
-lemma "\<not> (Suc 0 = Suc 1)" by eval
-lemma "[] = ([]\<Colon> int list)" by eval
+lemma "Suc 0 \<noteq> Suc 1" by eval
+lemma "[] = ([] :: int list)" by eval
 lemma "[()] = [()]" by eval
-lemma "fst ([]::nat list, Suc 0) = []" by eval
+lemma "fst ([] :: nat list, Suc 0) = []" by eval
 
 text {* SML evaluation oracle *}
 
 lemma "True \<or> False" by evaluation
-lemma "\<not> (Suc 0 = Suc 1)" by evaluation
-lemma "[] = ([]\<Colon> int list)" by evaluation
+lemma "Suc 0 \<noteq> Suc 1" by evaluation
+lemma "[] = ([] :: int list)" by evaluation
 lemma "[()] = [()]" by evaluation
-lemma "fst ([]::nat list, Suc 0) = []" by evaluation
+lemma "fst ([] :: nat list, Suc 0) = []" by evaluation
 
 text {* normalization *}
 
 lemma "True \<or> False" by normalization
-lemma "\<not> (Suc 0 = Suc 1)" by normalization
-lemma "[] = ([]\<Colon> int list)" by normalization
+lemma "Suc 0 \<noteq> Suc 1" by normalization
+lemma "[] = ([] :: int list)" by normalization
 lemma "[()] = [()]" by normalization
-lemma "fst ([]::nat list, Suc 0) = []" by normalization
+lemma "fst ([] :: nat list, Suc 0) = []" by normalization
 
 text {* term evaluation *}
 
@@ -47,10 +47,10 @@
 value [SML] "nat 100"
 value [nbe] "nat 100"
 
-value "(10\<Colon>int) \<le> 12"
-value [code] "(10\<Colon>int) \<le> 12"
-value [SML] "(10\<Colon>int) \<le> 12"
-value [nbe] "(10\<Colon>int) \<le> 12"
+value "(10::int) \<le> 12"
+value [code] "(10::int) \<le> 12"
+value [SML] "(10::int) \<le> 12"
+value [nbe] "(10::int) \<le> 12"
 
 value "max (2::int) 4"
 value [code] "max (2::int) 4"
@@ -62,29 +62,29 @@
 value [SML] "of_int 2 / of_int 4 * (1::rat)"
 value [nbe] "of_int 2 / of_int 4 * (1::rat)"
 
-value "[]::nat list"
-value [code] "[]::nat list"
-value [SML] "[]::nat list"
-value [nbe] "[]::nat list"
+value "[] :: nat list"
+value [code] "[] :: nat list"
+value [SML] "[] :: nat list"
+value [nbe] "[] :: nat list"
 
 value "[(nat 100, ())]"
 value [code] "[(nat 100, ())]"
 value [SML] "[(nat 100, ())]"
 value [nbe] "[(nat 100, ())]"
 
-
 text {* a fancy datatype *}
 
-datatype ('a, 'b) bair =
-    Bair "'a\<Colon>order" 'b
-  | Shift "('a, 'b) cair"
-  | Dummy unit
-and ('a, 'b) cair =
-    Cair 'a 'b
+datatype ('a, 'b) foo =
+    Foo "'a\<Colon>order" 'b
+  | Bla "('a, 'b) bar"
+  | Dummy nat
+and ('a, 'b) bar =
+    Bar 'a 'b
+  | Blubb "('a, 'b) foo"
 
-value "Shift (Cair (4::nat) [Suc 0])"
-value [code] "Shift (Cair (4::nat) [Suc 0])"
-value [SML] "Shift (Cair (4::nat) [Suc 0])"
-value [nbe] "Shift (Cair (4::nat) [Suc 0])"
+value "Bla (Bar (4::nat) [Suc 0])"
+value [code] "Bla (Bar (4::nat) [Suc 0])"
+value [SML] "Bla (Bar (4::nat) [Suc 0])"
+value [nbe] "Bla (Bar (4::nat) [Suc 0])"
 
 end
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/Pure/Concurrent/bash.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/bash.ML	Sat Nov 27 14:34:54 2010 -0800
@@ -0,0 +1,83 @@
+(*  Title:      Pure/Concurrent/bash.ML
+    Author:     Makarius
+
+GNU bash processes, with propagation of interrupts.
+*)
+
+val bash_output = uninterruptible (fn restore_attributes => fn script =>
+  let
+    datatype result = Wait | Signal | Result of int;
+    val result = Synchronized.var "bash_result" Wait;
+
+    val id = serial_string ();
+    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
+    val output_path = File.tmp_path (Path.basic ("bash_output" ^ id));
+    val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
+
+    val system_thread =
+      Simple_Thread.fork false (fn () =>
+        Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
+          let
+            val _ = File.write script_path script;
+            val status =
+              OS.Process.system
+                ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^
+                  File.shell_path pid_path ^ " script \"exec bash " ^
+                  File.shell_path script_path ^ " > " ^
+                  File.shell_path output_path ^ "\"");
+            val res =
+              (case Posix.Process.fromStatus status of
+                Posix.Process.W_EXITED => Result 0
+              | Posix.Process.W_EXITSTATUS 0wx82 => Signal
+              | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
+              | Posix.Process.W_SIGNALED s =>
+                  if s = Posix.Signal.int then Signal
+                  else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
+              | Posix.Process.W_STOPPED s =>
+                  Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
+          in Synchronized.change result (K res) end
+          handle _ (*sic*) => Synchronized.change result (fn Wait => Signal | res => res)));
+
+    fun terminate () =
+      let
+        val sig_test = Posix.Signal.fromWord 0w0;
+
+        fun kill_group pid s =
+          (Posix.Process.kill
+            (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true)
+          handle OS.SysErr _ => false;
+
+        fun kill s =
+          (case Int.fromString (File.read pid_path) of
+            NONE => true
+          | SOME pid => (kill_group pid s; kill_group pid sig_test))
+          handle IO.Io _ => true;
+
+        fun multi_kill count s =
+          count = 0 orelse
+            kill s andalso (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
+        val _ =
+          multi_kill 10 Posix.Signal.int andalso
+          multi_kill 10 Posix.Signal.term andalso
+          multi_kill 10 Posix.Signal.kill;
+      in () end;
+
+    fun cleanup () =
+     (terminate ();
+      Simple_Thread.interrupt system_thread;
+      try File.rm script_path;
+      try File.rm output_path;
+      try File.rm pid_path);
+  in
+    let
+      val _ =
+        restore_attributes (fn () =>
+          Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
+
+      val output = the_default "" (try File.read output_path);
+      val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
+      val _ = cleanup ();
+    in (output, rc) end
+    handle exn => (cleanup (); reraise exn)
+  end);
+
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/Pure/Concurrent/bash_sequential.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/bash_sequential.ML	Sat Nov 27 14:34:54 2010 -0800
@@ -0,0 +1,34 @@
+(*  Title:      Pure/Concurrent/bash_sequential.ML
+    Author:     Makarius
+
+Generic GNU bash processes (no provisions to propagate interrupts, but
+could work via the controlling tty).
+*)
+
+fun bash_output script =
+  let
+    val id = serial_string ();
+    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
+    val output_path = File.tmp_path (Path.basic ("bash_output" ^ id));
+    fun cleanup () = (try File.rm script_path; try File.rm output_path);
+  in
+    let
+      val _ = File.write script_path script;
+      val status =
+        OS.Process.system
+          ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
+            " script \"exec bash " ^ File.shell_path script_path ^ " > " ^
+            File.shell_path output_path ^ "\"");
+      val rc =
+        (case Posix.Process.fromStatus status of
+          Posix.Process.W_EXITED => 0
+        | Posix.Process.W_EXITSTATUS w => Word8.toInt w
+        | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
+        | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
+
+      val output = the_default "" (try File.read output_path);
+      val _ = cleanup ();
+    in (output, rc) end
+    handle exn => (cleanup (); reraise exn)
+  end;
+
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Sat Nov 27 14:09:03 2010 -0800
+++ b/src/Pure/General/file.ML	Sat Nov 27 14:34:54 2010 -0800
@@ -13,16 +13,9 @@
   val pwd: unit -> Path.T
   val full_path: Path.T -> Path.T
   val tmp_path: Path.T -> Path.T
-  val isabelle_tool: string -> string -> int
-  eqtype ident
-  val rep_ident: ident -> string
-  val ident: Path.T -> ident option
   val exists: Path.T -> bool
   val check: Path.T -> unit
   val rm: Path.T -> unit
-  val rm_tree: Path.T -> unit
-  val mkdir: Path.T -> unit
-  val mkdir_leaf: Path.T -> unit
   val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
   val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
   val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
@@ -35,7 +28,6 @@
   val write_buffer: Path.T -> Buffer.T -> unit
   val eq: Path.T * Path.T -> bool
   val copy: Path.T -> Path.T -> unit
-  val copy_dir: Path.T -> Path.T -> unit
 end;
 
 structure File: FILE =
@@ -45,7 +37,11 @@
 
 val platform_path = Path.implode o Path.expand;
 
-val shell_quote = enclose "'" "'";
+fun shell_quote s =
+  if exists_string (fn c => c = "'") s then
+    error ("Illegal single quote in path specification: " ^ quote s)
+  else enclose "'" "'" s;
+
 val shell_path = shell_quote o platform_path;
 
 
@@ -65,66 +61,6 @@
   Path.append (Path.variable "ISABELLE_TMP") (Path.base path);
 
 
-(* system commands *)
-
-fun isabelle_tool name args =
-  (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
-      let val path = dir ^ "/" ^ name in
-        if can OS.FileSys.modTime path andalso
-          not (OS.FileSys.isDir path) andalso
-          OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
-        then SOME path
-        else NONE
-      end handle OS.SysErr _ => NONE) of
-    SOME path => bash (shell_quote path ^ " " ^ args)
-  | NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
-
-fun system_command cmd =
-  if bash cmd <> 0 then error ("System command failed: " ^ cmd)
-  else ();
-
-
-(* file identification *)
-
-local
-  val ident_cache =
-    Unsynchronized.ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
-in
-
-fun check_cache (path, time) =
-  (case Symtab.lookup (! ident_cache) path of
-    NONE => NONE
-  | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE);
-
-fun update_cache (path, (time, id)) = CRITICAL (fn () =>
-  Unsynchronized.change ident_cache
-    (Symtab.update (path, {time_stamp = time, id = id})));
-
-end;
-
-datatype ident = Ident of string;
-fun rep_ident (Ident s) = s;
-
-fun ident path =
-  let val physical_path = perhaps (try OS.FileSys.fullPath) (platform_path path) in
-    (case try (Time.toString o OS.FileSys.modTime) physical_path of
-      NONE => NONE
-    | SOME mod_time => SOME (Ident
-        (case getenv "ISABELLE_FILE_IDENT" of
-          "" => physical_path ^ ": " ^ mod_time
-        | cmd =>
-            (case check_cache (physical_path, mod_time) of
-              SOME id => id
-            | NONE =>
-                let val (id, rc) =  (*potentially slow*)
-                  bash_output ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_quote physical_path)
-                in
-                  if id <> "" andalso rc = 0 then (update_cache (physical_path, (mod_time, id)); id)
-                  else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
-                end))))
-  end;
-
-
 (* directory entries *)
 
 val exists = can OS.FileSys.modTime o platform_path;
@@ -135,15 +71,6 @@
 
 val rm = OS.FileSys.remove o platform_path;
 
-fun rm_tree path = system_command ("rm -r " ^ shell_path path);
-
-fun mkdir path = system_command ("mkdir -p " ^ shell_path path);
-
-fun mkdir_leaf path = (check (Path.dir path); mkdir path);
-
-fun is_dir path =
-  the_default false (try OS.FileSys.isDir (platform_path path));
-
 
 (* open files *)
 
@@ -201,14 +128,13 @@
     SOME ids => is_equal (OS.FileSys.compare ids)
   | NONE => false);
 
+fun is_dir path =
+  the_default false (try OS.FileSys.isDir (platform_path path));
+
 fun copy src dst =
   if eq (src, dst) then ()
   else
     let val target = if is_dir dst then Path.append dst (Path.base src) else dst
     in write target (read src) end;
 
-fun copy_dir src dst =
-  if eq (src, dst) then ()
-  else (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ());
-
 end;
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Sat Nov 27 14:09:03 2010 -0800
+++ b/src/Pure/General/secure.ML	Sat Nov 27 14:34:54 2010 -0800
@@ -15,8 +15,6 @@
   val toplevel_pp: string list -> string -> unit
   val PG_setup: unit -> unit
   val commit: unit -> unit
-  val bash_output: string -> string * int
-  val bash: string -> int
 end;
 
 structure Secure: SECURE =
@@ -58,20 +56,6 @@
 fun PG_setup () =
   use_global "val change = Unsynchronized.change; structure ThyLoad = ProofGeneral.ThyLoad;";
 
-
-(* shell commands *)
-
-fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
-
-val orig_bash_output = bash_output;
-
-fun bash_output s = (secure_shell (); orig_bash_output s);
-
-fun bash s =
-  (case bash_output s of
-    ("", rc) => rc
-  | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
-
 end;
 
 (*override previous toplevel bindings!*)
@@ -80,5 +64,4 @@
 fun use s = Secure.use_file ML_Parse.global_context true s
   handle ERROR msg => (writeln msg; error "ML error");
 val toplevel_pp = Secure.toplevel_pp;
-val bash_output = Secure.bash_output;
-val bash = Secure.bash;
+
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Sat Nov 27 14:09:03 2010 -0800
+++ b/src/Pure/IsaMakefile	Sat Nov 27 14:34:54 2010 -0800
@@ -22,7 +22,6 @@
 BOOTSTRAP_FILES = 					\
   General/exn.ML					\
   General/timing.ML					\
-  ML-Systems/bash.ML 					\
   ML-Systems/compiler_polyml-5.2.ML			\
   ML-Systems/compiler_polyml-5.3.ML			\
   ML-Systems/ml_name_space.ML				\
@@ -55,6 +54,8 @@
 Pure: $(OUT)/Pure
 
 $(OUT)/Pure: $(BOOTSTRAP_FILES)				\
+  Concurrent/bash.ML 					\
+  Concurrent/bash_sequential.ML				\
   Concurrent/cache.ML					\
   Concurrent/future.ML					\
   Concurrent/lazy.ML					\
@@ -188,6 +189,7 @@
   Syntax/syntax.ML					\
   Syntax/type_ext.ML					\
   System/isabelle_process.ML				\
+  System/isabelle_system.ML				\
   System/isar.ML					\
   System/session.ML					\
   Thy/html.ML						\
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sat Nov 27 14:09:03 2010 -0800
+++ b/src/Pure/Isar/code.ML	Sat Nov 27 14:34:54 2010 -0800
@@ -316,7 +316,7 @@
     val data = case Datatab.lookup datatab kind
      of SOME data => data
       | NONE => invoke_init kind;
-    val result as (x, data') = f (dest data);
+    val result as (_, data') = f (dest data);
     val _ = Synchronized.change dataref
       ((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref));
   in result end;
@@ -358,11 +358,13 @@
  of SOME ty => ty
   | NONE => (Type.strip_sorts o Sign.the_const_type thy) c;
 
+fun args_number thy = length o fst o strip_type o const_typ thy;
+
 fun subst_signature thy c ty =
   let
-    fun mk_subst (Type (tyco, tys1)) (ty2 as Type (tyco2, tys2)) =
+    fun mk_subst (Type (_, tys1)) (Type (_, tys2)) =
           fold2 mk_subst tys1 tys2
-      | mk_subst ty (TVar (v, sort)) = Vartab.update (v, ([], ty))
+      | mk_subst ty (TVar (v, _)) = Vartab.update (v, ([], ty))
   in case lookup_typ thy c
    of SOME ty' => Envir.subst_type (mk_subst ty (expand_signature thy ty') Vartab.empty) ty'
     | NONE => ty
@@ -370,7 +372,10 @@
 
 fun subst_signatures thy = map_aterms (fn Const (c, ty) => Const (c, subst_signature thy c ty) | t => t);
 
-fun args_number thy = length o fst o strip_type o const_typ thy;
+fun logical_typscheme thy (c, ty) =
+  (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty);
+
+fun typscheme thy (c, ty) = logical_typscheme thy (c, subst_signature thy c ty);
 
 
 (* datatypes *)
@@ -407,13 +412,14 @@
         val _ = if (tyco' : string) <> tyco
           then error "Different type constructors in constructor set"
           else ();
-        val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
-      in ((tyco, sorts), c :: cs) end;
+        val sorts'' =
+          map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
+      in ((tyco, sorts''), c :: cs) end;
     fun inst vs' (c, (vs, ty)) =
       let
         val the_v = the o AList.lookup (op =) (vs ~~ vs');
         val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty;
-        val vs'' = map dest_TFree (Sign.const_typargs thy (c, ty'));
+        val (vs'', _) = logical_typscheme thy (c, ty');
       in (c, (vs'', (fst o strip_type) ty')) end;
     val c' :: cs' = map (ty_sorts thy) cs;
     val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
@@ -439,7 +445,7 @@
  
 fun get_type_of_constr_or_abstr thy c =
   case (snd o strip_type o const_typ thy) c
-   of Type (tyco, _) => let val ((vs, cos), abstract) = get_type thy tyco
+   of Type (tyco, _) => let val ((_, cos), abstract) = get_type thy tyco
         in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end
     | _ => NONE;
 
@@ -592,11 +598,6 @@
 fun const_abs_eqn thy = AxClass.unoverload_const thy o dest_Const o fst o strip_comb o snd
   o dest_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
 
-fun logical_typscheme thy (c, ty) =
-  (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty);
-
-fun typscheme thy (c, ty) = logical_typscheme thy (c, subst_signature thy c ty);
-
 fun mk_proj tyco vs ty abs rep =
   let
     val ty_abs = Type (tyco, map TFree vs);
@@ -641,19 +642,19 @@
     else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names)
   end;
 
-fun desymbolize_tvars thy thms =
+fun desymbolize_tvars thms =
   let
     val tvs = fold (Term.add_tvars o Thm.prop_of) thms [];
     val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs;
   in map (Thm.certify_instantiate (tvar_subst, [])) thms end;
 
-fun desymbolize_vars thy thm =
+fun desymbolize_vars thm =
   let
     val vs = Term.add_vars (Thm.prop_of thm) [];
     val var_subst = mk_desymbolization I I Var vs;
   in Thm.certify_instantiate ([], var_subst) thm end;
 
-fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy);
+fun canonize_thms thy = desymbolize_tvars #> same_arity thy #> map desymbolize_vars;
 
 
 (* abstype certificates *)
@@ -672,13 +673,12 @@
       then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep);
     val _ = check_decl_ty thy (abs, raw_ty);
     val _ = check_decl_ty thy (rep, rep_ty);
-    val var = (fst o dest_Var) param
+    val _ = (fst o dest_Var) param
       handle TERM _ => bad "Not an abstype certificate";
     val _ = if param = rhs then () else bad "Not an abstype certificate";
     val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy (abs, Logic.unvarifyT_global raw_ty);
     val ty = domain_type ty';
-    val vs' = map dest_TFree (Sign.const_typargs thy (abs, ty'));
-    val ty_abs = range_type ty';
+    val (vs', _) = logical_typscheme thy (abs, ty');
   in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end;
 
 
@@ -716,7 +716,7 @@
 
 fun concretify_abs thy tyco abs_thm =
   let
-    val (vs, ((c, _), (_, cert))) = get_abstype_spec thy tyco;
+    val (_, ((c, _), (_, cert))) = get_abstype_spec thy tyco;
     val lhs = (fst o Logic.dest_equals o Thm.prop_of) abs_thm
     val ty = fastype_of lhs;
     val ty_abs = (fastype_of o snd o dest_comb) lhs;
@@ -742,13 +742,16 @@
 
 fun empty_cert thy c = 
   let
-    val raw_ty = const_typ thy c;
-    val tvars = Term.add_tvar_namesT raw_ty [];
-    val tvars' = case AxClass.class_of_param thy c
-     of SOME class => [TFree (Name.aT, [class])]
-      | NONE => Name.invent_list [] Name.aT (length tvars)
-          |> map (fn v => TFree (v, []));
-    val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
+    val raw_ty = Logic.unvarifyT_global (const_typ thy c);
+    val (vs, _) = logical_typscheme thy (c, raw_ty);
+    val sortargs = case AxClass.class_of_param thy c
+     of SOME class => [[class]]
+      | NONE => (case get_type_of_constr_or_abstr thy c
+         of SOME (tyco, _) => (map snd o fst o the)
+              (AList.lookup (op =) ((snd o fst o get_type thy) tyco) c)
+          | NONE => replicate (length vs) []);
+    val the_sort = the o AList.lookup (op =) (map fst vs ~~ sortargs);
+    val ty = map_type_tfree (fn (v, _) => TFree (v, the_sort v)) raw_ty
     val chead = build_head thy (c, ty);
   in Equations (Thm.weaken chead Drule.dummy_thm, []) end;
 
@@ -767,19 +770,19 @@
           fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
         val sorts = map_transpose inter_sorts vss;
         val vts = Name.names Name.context Name.aT sorts;
-        val thms as thm :: _ =
+        val thms' =
           map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms;
-        val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms))));
+        val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms'))));
         fun head_conv ct = if can Thm.dest_comb ct
           then Conv.fun_conv head_conv ct
           else Conv.rewr_conv head_thm ct;
         val rewrite_head = Conv.fconv_rule (Conv.arg1_conv head_conv);
-        val cert_thm = Conjunction.intr_balanced (map rewrite_head thms);
+        val cert_thm = Conjunction.intr_balanced (map rewrite_head thms');
       in Equations (cert_thm, propers) end;
 
 fun cert_of_proj thy c tyco =
   let
-    val (vs, ((abs, (_, ty)), (rep, cert))) = get_abstype_spec thy tyco;
+    val (vs, ((abs, (_, ty)), (rep, _))) = get_abstype_spec thy tyco;
     val _ = if c = rep then () else
       error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy rep);
   in Projection (mk_proj tyco vs ty abs rep, tyco) end;
@@ -824,7 +827,7 @@
           Thm.prop_of cert_thm
           |> Logic.dest_conjunction_balanced (length propers);
       in (vs, fold (add_rhss_of_eqn thy) equations []) end
-  | typargs_deps_of_cert thy (Projection (t, tyco)) =
+  | typargs_deps_of_cert thy (Projection (t, _)) =
       (fst (typscheme_projection thy t), add_rhss_of_eqn thy t [])
   | typargs_deps_of_cert thy (Abstract (abs_thm, tyco)) =
       let
@@ -864,7 +867,7 @@
          o snd o equations_of_cert thy) cert
   | pretty_cert thy (Projection (t, _)) =
       [Syntax.pretty_term_global thy (map_types Logic.varifyT_global t)]
-  | pretty_cert thy (Abstract (abs_thm, tyco)) =
+  | pretty_cert thy (Abstract (abs_thm, _)) =
       [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT_global) abs_thm];
 
 fun bare_thms_of_cert thy (cert as Equations _) =
@@ -1118,7 +1121,7 @@
 
 fun del_eqn thm thy = case mk_eqn_liberal thy thm
  of SOME (thm, _) => let
-        fun del_eqn' (Default eqns) = empty_fun_spec
+        fun del_eqn' (Default _) = empty_fun_spec
           | del_eqn' (Eqns eqns) =
               Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns)
           | del_eqn' spec = spec
@@ -1130,7 +1133,7 @@
 
 (* cases *)
 
-fun case_cong thy case_const (num_args, (pos, constrs)) =
+fun case_cong thy case_const (num_args, (pos, _)) =
   let
     val ([x, y], ctxt) = Name.variants ["A", "A'"] Name.context;
     val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt;
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Nov 27 14:09:03 2010 -0800
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Nov 27 14:34:54 2010 -0800
@@ -291,11 +291,11 @@
 
 fun display_drafts files = Toplevel.imperative (fn () =>
   let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
-  in File.isabelle_tool "display" ("-c " ^ outfile ^ " &"); () end);
+  in Isabelle_System.isabelle_tool "display" ("-c " ^ outfile ^ " &"); () end);
 
 fun print_drafts files = Toplevel.imperative (fn () =>
   let val outfile = File.shell_path (Present.drafts "ps" files)
-  in File.isabelle_tool "print" ("-c " ^ outfile); () end);
+  in Isabelle_System.isabelle_tool "print" ("-c " ^ outfile); () end);
 
 
 (* print parts of theory and proof context *)
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/Pure/ML-Systems/bash.ML
--- a/src/Pure/ML-Systems/bash.ML	Sat Nov 27 14:09:03 2010 -0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(*  Title:      Pure/ML-Systems/bash.ML
-    Author:     Makarius
-
-Generic GNU bash processes (no provisions to propagate interrupts, but
-could work via the controlling tty).
-*)
-
-local
-
-fun read_file name =
-  let val is = TextIO.openIn name
-  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
-
-fun write_file name txt =
-  let val os = TextIO.openOut name
-  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
-
-in
-
-fun bash_output script =
-  let
-    val script_name = OS.FileSys.tmpName ();
-    val _ = write_file script_name script;
-
-    val output_name = OS.FileSys.tmpName ();
-
-    val status =
-      OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
-        " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
-    val rc =
-      (case Posix.Process.fromStatus status of
-        Posix.Process.W_EXITED => 0
-      | Posix.Process.W_EXITSTATUS w => Word8.toInt w
-      | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
-      | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
-
-    val output = read_file output_name handle IO.Io _ => "";
-    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
-    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
-  in (output, rc) end;
-
-end;
-
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Nov 27 14:09:03 2010 -0800
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Nov 27 14:34:54 2010 -0800
@@ -8,7 +8,6 @@
 sig
   val interruptible: ('a -> 'b) -> 'a -> 'b
   val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
-  val bash_output: string -> string * int
   structure TimeLimit: TIME_LIMIT
 end;
 
@@ -42,20 +41,6 @@
 fun enabled () = max_threads_value () > 1;
 
 
-(* misc utils *)
-
-fun show "" = "" | show name = " " ^ name;
-fun show' "" = "" | show' name = " [" ^ name ^ "]";
-
-fun read_file name =
-  let val is = TextIO.openIn name
-  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
-
-fun write_file name txt =
-  let val os = TextIO.openOut name
-  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
-
-
 (* thread attributes *)
 
 val no_interrupts =
@@ -156,71 +141,6 @@
 end;
 
 
-(* GNU bash processes, with propagation of interrupts *)
-
-fun bash_output script = with_attributes no_interrupts (fn orig_atts =>
-  let
-    val script_name = OS.FileSys.tmpName ();
-    val _ = write_file script_name script;
-
-    val pid_name = OS.FileSys.tmpName ();
-    val output_name = OS.FileSys.tmpName ();
-
-    (*result state*)
-    datatype result = Wait | Signal | Result of int;
-    val result = ref Wait;
-    val lock = Mutex.mutex ();
-    val cond = ConditionVar.conditionVar ();
-    fun set_result res =
-      (Mutex.lock lock; result := res; ConditionVar.signal cond; Mutex.unlock lock);
-
-    val _ = Mutex.lock lock;
-
-    (*system thread*)
-    val system_thread = Thread.fork (fn () =>
-      let
-        val status =
-          OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^
-            " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
-        val res =
-          (case Posix.Process.fromStatus status of
-            Posix.Process.W_EXITED => Result 0
-          | Posix.Process.W_EXITSTATUS 0wx82 => Signal
-          | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
-          | Posix.Process.W_SIGNALED s =>
-              if s = Posix.Signal.int then Signal
-              else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
-          | Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
-      in set_result res end handle _ (*sic*) => set_result (Result 2), []);
-
-    (*main thread -- proxy for interrupts*)
-    fun kill n =
-      (case Int.fromString (read_file pid_name) of
-        SOME pid =>
-          Posix.Process.kill
-            (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)),
-              Posix.Signal.int)
-      | NONE => ())
-      handle OS.SysErr _ => () | IO.Io _ =>
-        (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ());
-
-    val _ =
-      while ! result = Wait do
-        let val res =
-          sync_wait (SOME orig_atts)
-            (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock
-        in if Exn.is_interrupt_exn res then kill 10 else () end;
-
-    (*cleanup*)
-    val output = read_file output_name handle IO.Io _ => "";
-    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
-    val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
-    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
-    val _ = Thread.interrupt system_thread handle Thread _ => ();
-    val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc);
-  in (output, rc) end);
-
-
 (* critical section -- may be nested within the same thread *)
 
 local
@@ -229,6 +149,9 @@
 val critical_thread = ref (NONE: Thread.thread option);
 val critical_name = ref "";
 
+fun show "" = "" | show name = " " ^ name;
+fun show' "" = "" | show' name = " [" ^ name ^ "]";
+
 in
 
 fun self_critical () =
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Sat Nov 27 14:09:03 2010 -0800
+++ b/src/Pure/ML-Systems/polyml_common.ML	Sat Nov 27 14:34:54 2010 -0800
@@ -14,7 +14,6 @@
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
 use "General/timing.ML";
-use "ML-Systems/bash.ML";
 use "ML-Systems/ml_pretty.ML";
 use "ML-Systems/use_context.ML";
 
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/Pure/ML-Systems/proper_int.ML
--- a/src/Pure/ML-Systems/proper_int.ML	Sat Nov 27 14:09:03 2010 -0800
+++ b/src/Pure/ML-Systems/proper_int.ML	Sat Nov 27 14:34:54 2010 -0800
@@ -165,6 +165,15 @@
   val fromInt = Word.fromInt o dest_int;
 end;
 
+structure Word8 =
+struct
+  open Word8;
+  val wordSize = mk_int Word8.wordSize;
+  val toInt = mk_int o Word8.toInt;
+  val toIntX = mk_int o Word8.toIntX;
+  val fromInt = Word8.fromInt o dest_int;
+end;
+
 structure Word32 =
 struct
   open Word32;
@@ -174,6 +183,15 @@
   val fromInt = Word32.fromInt o dest_int;
 end;
 
+structure LargeWord =
+struct
+  open LargeWord;
+  val wordSize = mk_int LargeWord.wordSize;
+  val toInt = mk_int o LargeWord.toInt;
+  val toIntX = mk_int o LargeWord.toIntX;
+  val fromInt = LargeWord.fromInt o dest_int;
+end;
+
 
 (* Real *)
 
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Sat Nov 27 14:09:03 2010 -0800
+++ b/src/Pure/ML-Systems/smlnj.ML	Sat Nov 27 14:34:54 2010 -0800
@@ -14,7 +14,6 @@
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/multithreading.ML";
 use "General/timing.ML";
-use "ML-Systems/bash.ML";
 use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/ml_pretty.ML";
 structure PolyML = struct end;
@@ -170,11 +169,6 @@
 val pwd = OS.FileSys.getDir;
 
 
-(* system command execution *)
-
-val bash_output = (fn (output, rc) => (output, mk_int rc)) o bash_output;
-
-
 (* getenv *)
 
 fun getenv var =
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Nov 27 14:09:03 2010 -0800
+++ b/src/Pure/ROOT.ML	Sat Nov 27 14:34:54 2010 -0800
@@ -72,6 +72,15 @@
 if Multithreading.available then ()
 else use "Concurrent/synchronized_sequential.ML";
 
+if Multithreading.available
+then use "Concurrent/bash.ML"
+else use "Concurrent/bash_sequential.ML";
+
+fun bash s =
+  (case bash_output s of
+    ("", rc) => rc
+  | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
+
 use "Concurrent/mailbox.ML";
 use "Concurrent/task_queue.ML";
 use "Concurrent/future.ML";
@@ -233,6 +242,7 @@
 use "Isar/toplevel.ML";
 
 (*theory documents*)
+use "System/isabelle_system.ML";
 use "Thy/present.ML";
 use "Thy/term_style.ML";
 use "Thy/thy_output.ML";
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/Pure/System/isabelle_system.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/isabelle_system.ML	Sat Nov 27 14:34:54 2010 -0800
@@ -0,0 +1,51 @@
+(*  Title:      Pure/System/isabelle_system.ML
+    Author:     Makarius
+
+Isabelle system support.
+*)
+
+signature ISABELLE_SYSTEM =
+sig
+  val isabelle_tool: string -> string -> int
+  val rm_tree: Path.T -> unit
+  val mkdirs: Path.T -> unit
+  val mkdir: Path.T -> unit
+  val copy_dir: Path.T -> Path.T -> unit
+end;
+
+structure Isabelle_System: ISABELLE_SYSTEM =
+struct
+
+(* system commands *)
+
+fun isabelle_tool name args =
+  (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
+      let val path = dir ^ "/" ^ name in
+        if can OS.FileSys.modTime path andalso
+          not (OS.FileSys.isDir path) andalso
+          OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
+        then SOME path
+        else NONE
+      end handle OS.SysErr _ => NONE) of
+    SOME path => bash (File.shell_quote path ^ " " ^ args)
+  | NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
+
+fun system_command cmd =
+  if bash cmd <> 0 then error ("System command failed: " ^ cmd)
+  else ();
+
+
+(* directory operations *)
+
+fun rm_tree path = system_command ("rm -r " ^ File.shell_path path);
+
+fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
+
+val mkdir = OS.FileSys.mkDir o File.platform_path;
+
+fun copy_dir src dst =
+  if File.eq (src, dst) then ()
+  else (system_command ("cp -r -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
+
+end;
+
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sat Nov 27 14:09:03 2010 -0800
+++ b/src/Pure/Thy/present.ML	Sat Nov 27 14:34:54 2010 -0800
@@ -94,7 +94,7 @@
     val _ = writeln "Displaying graph ...";
     val path = File.tmp_path (Path.explode "tmp.graph");
     val _ = write_graph gr path;
-    val _ = File.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
+    val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
   in () end;
 
 
@@ -344,7 +344,7 @@
     val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path gr_path;
   in
     write_graph graph gr_path;
-    if File.isabelle_tool "browser" args <> 0 orelse
+    if Isabelle_System.isabelle_tool "browser" args <> 0 orelse
       not (File.exists eps_path) orelse not (File.exists pdf_path)
     then error "Failed to prepare dependency graph"
     else
@@ -384,9 +384,9 @@
       else NONE;
 
     fun prepare_sources cp path =
-     (File.mkdir path;
-      if cp then File.copy_dir document_path path else ();
-      File.isabelle_tool "latex"
+     (Isabelle_System.mkdirs path;
+      if cp then Isabelle_System.copy_dir document_path path else ();
+      Isabelle_System.isabelle_tool "latex"
         ("-o sty " ^ File.shell_path (Path.append path (Path.basic "root.tex")));
       (case opt_graphs of NONE => () | SOME (pdf, eps) =>
         (File.write (Path.append path graph_pdf_path) pdf;
@@ -395,14 +395,14 @@
       List.app (finish_tex path) thys);
   in
     if info then
-     (File.mkdir (Path.append html_prefix session_path);
+     (Isabelle_System.mkdirs (Path.append html_prefix session_path);
       File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index);
       File.write (Path.append html_prefix session_entries_path) "";
       create_index html_prefix;
       if length path > 1 then update_index parent_html_prefix name else ();
       (case readme of NONE => () | SOME path => File.copy path html_prefix);
       write_graph sorted_graph (Path.append html_prefix graph_path);
-      File.isabelle_tool "browser" "-b";
+      Isabelle_System.isabelle_tool "browser" "-b";
       File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
       List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
         (HTML.applet_pages name (Url.File index_path, name));
@@ -509,11 +509,11 @@
 
     val doc_path = File.tmp_path document_path;
     val result_path = Path.append doc_path Path.parent;
-    val _ = File.mkdir doc_path;
+    val _ = Isabelle_System.mkdirs doc_path;
     val root_path = Path.append doc_path (Path.basic "root.tex");
     val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path;
-    val _ = File.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path);
-    val _ = File.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path);
+    val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path);
+    val _ = Isabelle_System.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path);
 
     fun known name =
       let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Nov 27 14:09:03 2010 -0800
+++ b/src/Pure/Thy/thy_info.ML	Sat Nov 27 14:34:54 2010 -0800
@@ -64,8 +64,8 @@
 (* thy database *)
 
 type deps =
- {master: (Path.T * File.ident),  (*master dependencies for thy file*)
-  imports: string list};          (*source specification of imports (partially qualified)*)
+ {master: (Path.T * Thy_Load.file_ident),  (*master dependencies for thy file*)
+  imports: string list};  (*source specification of imports (partially qualified)*)
 
 fun make_deps master imports : deps = {master = master, imports = imports};
 
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Sat Nov 27 14:09:03 2010 -0800
+++ b/src/Pure/Thy/thy_load.ML	Sat Nov 27 14:34:54 2010 -0800
@@ -17,14 +17,17 @@
 signature THY_LOAD =
 sig
   include BASIC_THY_LOAD
+  eqtype file_ident
+  val pretty_file_ident: file_ident -> Pretty.T
+  val file_ident: Path.T -> file_ident option
   val set_master_path: Path.T -> unit
   val get_master_path: unit -> Path.T
   val master_directory: theory -> Path.T
-  val provide: Path.T * (Path.T * File.ident) -> theory -> theory
-  val check_file: Path.T list -> Path.T -> Path.T * File.ident
-  val check_thy: Path.T -> string -> Path.T * File.ident
+  val provide: Path.T * (Path.T * file_ident) -> theory -> theory
+  val check_file: Path.T list -> Path.T -> Path.T * file_ident
+  val check_thy: Path.T -> string -> Path.T * file_ident
   val deps_thy: Path.T -> string ->
-   {master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list}
+   {master: Path.T * file_ident, text: string, imports: string list, uses: Path.T list}
   val loaded_files: theory -> Path.T list
   val all_current: theory -> bool
   val provide_file: Path.T -> theory -> theory
@@ -36,12 +39,57 @@
 structure Thy_Load: THY_LOAD =
 struct
 
+(* file identification *)
+
+local
+  val file_ident_cache =
+    Synchronized.var "file_ident_cache"
+      (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
+in
+
+fun check_cache (path, time) =
+  (case Symtab.lookup (Synchronized.value file_ident_cache) path of
+    NONE => NONE
+  | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE);
+
+fun update_cache (path, (time, id)) =
+  Synchronized.change file_ident_cache
+    (Symtab.update (path, {time_stamp = time, id = id}));
+
+end;
+
+datatype file_ident = File_Ident of string;
+
+fun pretty_file_ident (File_Ident s) = Pretty.str (quote s);
+
+fun file_ident path =
+  let val physical_path = perhaps (try OS.FileSys.fullPath) (File.platform_path path) in
+    (case try (Time.toString o OS.FileSys.modTime) physical_path of
+      NONE => NONE
+    | SOME mod_time => SOME (File_Ident
+        (case getenv "ISABELLE_FILE_IDENT" of
+          "" => physical_path ^ ": " ^ mod_time
+        | cmd =>
+            (case check_cache (physical_path, mod_time) of
+              SOME id => id
+            | NONE =>
+                let
+                  val (id, rc) =  (*potentially slow*)
+                    bash_output
+                      ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ File.shell_quote physical_path);
+                in
+                  if id <> "" andalso rc = 0 then (update_cache (physical_path, (mod_time, id)); id)
+                  else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
+                end))))
+  end;
+
+
 (* manage source files *)
 
 type files =
- {master_dir: Path.T,                                 (*master directory of theory source*)
-  required: Path.T list,                              (*source path*)
-  provided: (Path.T * (Path.T * File.ident)) list};   (*source path, physical path, identifier*)
+ {master_dir: Path.T,  (*master directory of theory source*)
+  required: Path.T list,  (*source path*)
+  provided: (Path.T * (Path.T * file_ident)) list};  (*source path, physical path, identifier*)
 
 fun make_files (master_dir, required, provided): files =
  {master_dir = master_dir, required = required, provided = provided};
@@ -79,26 +127,26 @@
 (* maintain default paths *)
 
 local
-  val load_path = Unsynchronized.ref [Path.current];
+  val load_path = Synchronized.var "load_path" [Path.current];
   val master_path = Unsynchronized.ref Path.current;
 in
 
-fun show_path () = map Path.implode (! load_path);
+fun show_path () = map Path.implode (Synchronized.value load_path);
 
-fun del_path s =
-  CRITICAL (fn () => Unsynchronized.change load_path (remove (op =) (Path.explode s)));
+fun del_path s = Synchronized.change load_path (remove (op =) (Path.explode s));
 
-fun add_path s =
-  CRITICAL (fn () => (del_path s; Unsynchronized.change load_path (cons (Path.explode s))));
+fun add_path s = Synchronized.change load_path (update (op =) (Path.explode s));
 
 fun path_add s =
-  CRITICAL (fn () =>
-    (del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s])));
+  Synchronized.change load_path (fn path =>
+    let val p = Path.explode s
+    in remove (op =) p path @ [p] end);
 
-fun reset_path () = CRITICAL (fn () => load_path := [Path.current]);
+fun reset_path () = Synchronized.change load_path (K [Path.current]);
 
 fun search_path dir path =
-  distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));
+  distinct (op =)
+    (dir :: (if Path.is_basic path then (Synchronized.value load_path) else [Path.current]));
 
 fun set_master_path path = master_path := path;
 fun get_master_path () = ! master_path;
@@ -115,7 +163,7 @@
   in
     dirs |> get_first (fn dir =>
       let val full_path = File.full_path (Path.append dir path) in
-        (case File.ident full_path of
+        (case file_ident full_path of
           NONE => NONE
         | SOME id => SOME (full_path, id))
       end)
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Sat Nov 27 14:09:03 2010 -0800
+++ b/src/Pure/pure_setup.ML	Sat Nov 27 14:34:54 2010 -0800
@@ -36,7 +36,7 @@
 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
 toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
 toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
-toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
+toplevel_pp ["Thy_Load", "file_ident"] "Thy_Load.pretty_file_ident";
 toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
 
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Sat Nov 27 14:09:03 2010 -0800
+++ b/src/Tools/Code/code_haskell.ML	Sat Nov 27 14:34:54 2010 -0800
@@ -353,7 +353,7 @@
             val _ = File.check destination;
             val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode
               o separate "/" o Long_Name.explode) module_name;
-            val _ = File.mkdir_leaf (Path.dir filepath);
+            val _ = Isabelle_System.mkdir (Path.dir filepath);
           in
             (File.write filepath o format [] width o Pretty.chunks2)
               [str "{-# OPTIONS_GHC -fglasgow-exts #-}", content]
diff -r c8b52f9e1680 -r 6c12f5e24e34 src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Sat Nov 27 14:09:03 2010 -0800
+++ b/src/Tools/cache_io.ML	Sat Nov 27 14:34:54 2010 -0800
@@ -44,9 +44,9 @@
 fun with_tmp_dir name f =
   let
     val path = File.tmp_path (Path.explode (name ^ serial_string ()))
-    val _ = File.mkdir path
+    val _ = Isabelle_System.mkdirs path
     val x = Exn.capture f path
-    val _ = try File.rm_tree path
+    val _ = try Isabelle_System.rm_tree path
   in Exn.release x end
 
 type result = {