# HG changeset patch
# User wenzelm
# Date 1117729795 -7200
# Node ID 0eb3c15298cd467d55afa311e37272850898fd03
# Parent  3d192ab9907b42a16daf7b0dda9f4d463e8d355a
tuned;

diff -r 3d192ab9907b -r 0eb3c15298cd src/Pure/General/url.ML
--- a/src/Pure/General/url.ML	Thu Jun 02 18:29:54 2005 +0200
+++ b/src/Pure/General/url.ML	Thu Jun 02 18:29:55 2005 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Basic URLs.  See RFC 1738.
+Basic URLs, see RFC 1738.
 *)
 
 signature URL =
@@ -52,22 +52,21 @@
 
 local
 
-fun gen_host quant = (quant (not_equal "/" andf Symbol.not_eof) >> implode) --|
+val scan_host =
+  (Scan.any1 (not_equal "/" andf Symbol.not_eof) >> implode) --|
   Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
 
-val scan_host1 = gen_host Scan.any1;
 val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
-val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o (curry (op^) "/") o implode);
+val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o implode o cons "/");
 
 val scan_url =
   Scan.unless (Scan.this_string "file:" ||
     Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File ||
   Scan.this_string "file:///" |-- scan_path_root >> File ||
   Scan.this_string "file://localhost/" |-- scan_path_root >> File ||
-  Scan.this_string "file://" |-- scan_host1 -- scan_path >> RemoteFile ||
-  Scan.this_string "http://" |-- scan_host1 -- scan_path >> Http ||
-  Scan.this_string "ftp://" |-- scan_host1 -- scan_path >> Ftp ||
-  Scan.this_string "file://" |-- scan_host1 -- scan_path >> Ftp (* or other proto *)
+  Scan.this_string "file://" |-- scan_host -- scan_path >> RemoteFile ||
+  Scan.this_string "http://" |-- scan_host -- scan_path >> Http ||
+  Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp;
 
 in
 
diff -r 3d192ab9907b -r 0eb3c15298cd src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Jun 02 18:29:54 2005 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Jun 02 18:29:55 2005 +0200
@@ -64,9 +64,8 @@
   val deps_thy: string -> bool -> Path.T -> string list * Path.T list
   val load_thy: string -> bool -> bool -> Path.T -> unit
   val isar: bool -> bool -> unit Toplevel.isar
-  val scan: string -> OuterLex.token list  
-  val read: OuterLex.token list -> 
-		(string * OuterLex.token list * Toplevel.transition) list
+  val scan: string -> OuterLex.token list
+  val read: OuterLex.token list -> (string * OuterLex.token list * Toplevel.transition) list
 end;
 
 structure OuterSyntax : OUTER_SYNTAX  =
@@ -268,13 +267,16 @@
   |> toplevel_source term false true get_parser;
 
 
-(* scan text,  read tokens with trace (for Proof General) *)
+(* scan text *)
 
 fun scan str =
- Source.of_string str
- |> Symbol.source false
- |> T.source true get_lexicons Position.none
- |> Source.exhaust
+  Source.of_string str
+  |> Symbol.source false
+  |> T.source true get_lexicons Position.none
+  |> Source.exhaust;
+
+
+(* read tokens with trace *)
 
 fun read toks =
   Source.of_list toks
@@ -283,6 +285,7 @@
   |> map (fn tr => (Toplevel.name_of tr, the (Toplevel.source_of tr), tr));
 
 
+
 (** read theory **)
 
 (* check_text *)
diff -r 3d192ab9907b -r 0eb3c15298cd src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Thu Jun 02 18:29:54 2005 +0200
+++ b/src/Pure/Proof/extraction.ML	Thu Jun 02 18:29:55 2005 +0200
@@ -123,14 +123,10 @@
 
 val chtype = change_type o SOME;
 
-fun add_prefix a b = NameSpace.pack (a :: NameSpace.unpack b);
+fun extr_name s vs = NameSpace.append "extr" (space_implode "_" (s :: vs));
+fun corr_name s vs = extr_name s vs ^ "_correctness";
 
-fun corr_name s vs =
-  add_prefix "extr" (space_implode "_" (s :: vs)) ^ "_correctness";
-
-fun extr_name s vs = add_prefix "extr" (space_implode "_" (s :: vs));
-
-fun msg d s = priority (implode (replicate d " ") ^ s);
+fun msg d s = priority (Symbol.spaces d ^ s);
 
 fun vars_of t = rev (foldl_aterms
   (fn (vs, v as Var _) => v ins vs | (vs, _) => vs) ([], t));
@@ -279,7 +275,7 @@
 val add_typeof_eqns = gen_add_typeof_eqns read_condeq;
 
 fun thaw (T as TFree (a, S)) =
-      if ":" mem explode a then TVar (unpack_ixn a, S) else T
+      if exists_string (equal ":") a then TVar (unpack_ixn a, S) else T
   | thaw (Type (a, Ts)) = Type (a, map thaw Ts)
   | thaw T = T;
 
diff -r 3d192ab9907b -r 0eb3c15298cd src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Thu Jun 02 18:29:54 2005 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Thu Jun 02 18:29:55 2005 +0200
@@ -37,10 +37,10 @@
 
 (** constants for theorems and axioms **)
 
-fun add_prefix a b = NameSpace.pack (a :: NameSpace.unpack b);
-
-fun add_proof_atom_consts names sg = Sign.add_consts_i
-  (map (fn name => (name, proofT, NoSyn)) names) (Sign.add_path "//" sg);
+fun add_proof_atom_consts names sg =
+  sg
+  |> Sign.add_path "//"
+  |> Sign.add_consts_i (map (fn name => (name, proofT, NoSyn)) names);
 
 (** constants for application and abstraction **)
 
@@ -184,12 +184,12 @@
   [proofT, itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
 
 fun term_of _ (PThm ((name, _), _, _, NONE)) =
-      Const (add_prefix "thm" name, proofT)
+      Const (NameSpace.append "thm" name, proofT)
   | term_of _ (PThm ((name, _), _, _, SOME Ts)) =
-      mk_tyapp (Const (add_prefix "thm" name, proofT), Ts)
-  | term_of _ (PAxm (name, _, NONE)) = Const (add_prefix "axm" name, proofT)
+      mk_tyapp (Const (NameSpace.append "thm" name, proofT), Ts)
+  | term_of _ (PAxm (name, _, NONE)) = Const (NameSpace.append "axm" name, proofT)
   | term_of _ (PAxm (name, _, SOME Ts)) =
-      mk_tyapp (Const (add_prefix "axm" name, proofT), Ts)
+      mk_tyapp (Const (NameSpace.append "axm" name, proofT), Ts)
   | term_of _ (PBound i) = Bound i
   | term_of Ts (Abst (s, opT, prf)) = 
       let val T = getOpt (opT,dummyT)
@@ -223,7 +223,7 @@
     val sg = sign_of thy |>
       add_proof_syntax |>
       add_proof_atom_consts
-        (map (add_prefix "axm") axm_names @ map (add_prefix "thm") thm_names)
+        (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names)
   in
     (cterm_of sg (term_of_proof prf'),
      proof_of_term thy tab true o Thm.term_of)
@@ -237,7 +237,7 @@
     val sg = sign_of thy |>
       add_proof_syntax |>
       add_proof_atom_consts
-        (map (add_prefix "axm") axm_names @ map (add_prefix "thm") thm_names)
+        (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names)
   in
     (fn T => fn s => Thm.term_of (read_cterm sg (s, T)))
   end;
@@ -255,7 +255,7 @@
     val sg' = sg |>
       add_proof_syntax |>
       add_proof_atom_consts
-        (map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)
+        (map (NameSpace.append "thm") thm_names @ map (NameSpace.append "axm") axm_names)
   in
     Sign.pretty_term sg' (term_of_proof prf)
   end;
diff -r 3d192ab9907b -r 0eb3c15298cd src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Thu Jun 02 18:29:54 2005 +0200
+++ b/src/Pure/type_infer.ML	Thu Jun 02 18:29:55 2005 +0200
@@ -88,13 +88,13 @@
   | deref (Link (ref T)) = deref T
   | deref T = T;
 
-fun foldl_pretyps f (x, PConst (_, T)) = f (x, T)
-  | foldl_pretyps f (x, PFree (_, T)) = f (x, T)
-  | foldl_pretyps f (x, PVar (_, T)) = f (x, T)
-  | foldl_pretyps _ (x, PBound _) = x
-  | foldl_pretyps f (x, PAbs (_, T, t)) = foldl_pretyps f (f (x, T), t)
-  | foldl_pretyps f (x, PAppl (t, u)) = foldl_pretyps f (foldl_pretyps f (x, t), u)
-  | foldl_pretyps f (x, Constraint (t, T)) = f (foldl_pretyps f (x, t), T);
+fun fold_pretyps f (PConst (_, T)) x = f T x
+  | fold_pretyps f (PFree (_, T)) x = f T x
+  | fold_pretyps f (PVar (_, T)) x = f T x
+  | fold_pretyps _ (PBound _) x = x
+  | fold_pretyps f (PAbs (_, T, t)) x = fold_pretyps f t (f T x)
+  | fold_pretyps f (PAppl (t, u)) x = fold_pretyps f u (fold_pretyps f t x)
+  | fold_pretyps f (Constraint (t, T)) x = f T (fold_pretyps f t x);
 
 
 
@@ -110,16 +110,16 @@
 
 fun pretyp_of is_param (params, typ) =
   let
-    fun add_parms (ps, TVar (xi as (x, _), S)) =
-          if is_param xi andalso is_none (assoc (ps, xi))
+    fun add_parms (TVar (xi as (x, _), S)) ps =
+          if is_param xi andalso is_none (assoc_string_int (ps, xi))
           then (xi, mk_param S) :: ps else ps
-      | add_parms (ps, TFree _) = ps
-      | add_parms (ps, Type (_, Ts)) = Library.foldl add_parms (ps, Ts);
+      | add_parms (TFree _) ps = ps
+      | add_parms (Type (_, Ts)) ps = fold add_parms Ts ps;
 
-    val params' = add_parms (params, typ);
+    val params' = add_parms typ params;
 
     fun pre_of (TVar (v as (xi, _))) =
-          (case assoc (params', xi) of
+          (case assoc_string_int (params', xi) of
             NONE => PTVar v
           | SOME p => p)
       | pre_of (TFree ("'_dummy_", S)) = mk_param S
@@ -137,7 +137,7 @@
 fun preterm_of const_type is_param ((vparams, params), tm) =
   let
     fun add_vparm (ps, xi) =
-      if is_none (assoc (ps, xi)) then
+      if is_none (assoc_string_int (ps, xi)) then
         (xi, mk_param []) :: ps
       else ps;
 
@@ -149,7 +149,7 @@
       | add_vparms (ps, _) = ps;
 
     val vparams' = add_vparms (vparams, tm);
-    fun var_param xi = valOf (assoc (vparams', xi));
+    fun var_param xi = the (assoc_string_int (vparams', xi));
 
 
     val preT_of = pretyp_of is_param;
@@ -192,23 +192,23 @@
 
 (* add_parms *)
 
-fun add_parmsT (rs, PType (_, Ts)) = Library.foldl add_parmsT (rs, Ts)
-  | add_parmsT (rs, Link (r as ref (Param _))) = r ins rs
-  | add_parmsT (rs, Link (ref T)) = add_parmsT (rs, T)
-  | add_parmsT (rs, _) = rs;
+fun add_parmsT (PType (_, Ts)) rs = fold add_parmsT Ts rs
+  | add_parmsT (Link (r as ref (Param _))) rs = r ins rs
+  | add_parmsT (Link (ref T)) rs = add_parmsT T rs
+  | add_parmsT _ rs = rs;
 
-val add_parms = foldl_pretyps add_parmsT;
+val add_parms = fold_pretyps add_parmsT;
 
 
 (* add_names *)
 
-fun add_namesT (xs, PType (_, Ts)) = Library.foldl add_namesT (xs, Ts)
-  | add_namesT (xs, PTFree (x, _)) = x ins xs
-  | add_namesT (xs, PTVar ((x, _), _)) = x ins xs
-  | add_namesT (xs, Link (ref T)) = add_namesT (xs, T)
-  | add_namesT (xs, Param _) = xs;
+fun add_namesT (PType (_, Ts)) xs = fold add_namesT Ts xs
+  | add_namesT (PTFree (x, _)) xs = x ins_string xs
+  | add_namesT (PTVar ((x, _), _)) xs = x ins_string xs
+  | add_namesT (Link (ref T)) xs = add_namesT T xs
+  | add_namesT (Param _) xs = xs;
 
-val add_names = foldl_pretyps add_namesT;
+val add_names = fold_pretyps add_namesT;
 
 
 (* simple_typ/term_of *)
@@ -237,11 +237,11 @@
     fun elim (r as ref (Param S), x) = r := mk_var (x, S)
       | elim _ = ();
 
-    val used' = Library.foldl add_names (Library.foldl add_namesT (used, Ts), ts);
-    val parms = rev (Library.foldl add_parms (Library.foldl add_parmsT ([], Ts), ts));
+    val used' = fold add_names ts (fold add_namesT Ts used);
+    val parms = rev (fold add_parms ts (fold add_parmsT Ts []));
     val names = Term.invent_names used' (prfx ^ "'a") (length parms);
   in
-    seq2 elim (parms, names);
+    ListPair.app elim (parms, names);
     (map simple_typ_of Ts, map simple_term_of ts)
   end;
 
@@ -269,7 +269,7 @@
           else r := mk_param (Sorts.inter_sort classes (S', S))
       | meet (Link (ref T), S) = meet (T, S)
       | meet (PType (a, Ts), S) =
-          seq2 meet (Ts, Sorts.mg_domain (classes, arities) a S
+          ListPair.app meet (Ts, Sorts.mg_domain (classes, arities) a S
             handle Sorts.DOMAIN ac => raise NO_UNIFIER (no_domain ac))
       | meet (PTFree (x, S'), S) =
           if Sorts.sort_le classes (S', S) then ()
@@ -304,7 +304,7 @@
       | unif (PType (a, Ts), PType (b, Us)) =
           if a <> b then
             raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b)
-          else seq2 unif (Ts, Us)
+          else ListPair.app unif (Ts, Us)
       | unif (T, U) = if T = U then () else raise NO_UNIFIER "";
 
   in unif end;
@@ -457,7 +457,7 @@
           ^ commas_quote (map (Syntax.string_of_vname' o fst) dups)));
 
     fun get xi =
-      (case (assoc (env, xi), def_sort xi) of
+      (case (assoc_string_int (env, xi), def_sort xi) of
         (NONE, NONE) => Type.defaultS tsig
       | (NONE, SOME S) => S
       | (SOME S, NONE) => S
@@ -472,8 +472,8 @@
 
 fun decode_types tsig is_const def_type def_sort map_const map_type map_sort tm =
   let
-    fun get_type xi = getOpt (def_type xi, dummyT);
-    fun is_free x = isSome (def_type (x, ~1));
+    fun get_type xi = if_none (def_type xi) dummyT;
+    fun is_free x = is_some (def_type (x, ~1));
     val raw_env = Syntax.raw_term_sorts tm;
     val sort_of = get_sort tsig def_sort map_sort raw_env;
 
@@ -509,8 +509,8 @@
 
   tsig: type signature
   const_type: name mapping and signature lookup
-  def_type: partial map from indexnames to types (constrains Frees, Vars)
-  def_sort: partial map from indexnames to sorts (constrains TFrees, TVars)
+  def_type: partial map from indexnames to types (constrains Frees and Vars)
+  def_sort: partial map from indexnames to sorts (constrains TFrees and TVars)
   used: list of already used type variables
   freeze: if true then generated parameters are turned into TFrees, else TVars*)
 
@@ -519,7 +519,7 @@
   let
     val {classes, arities, ...} = Type.rep_tsig tsig;
     val pat_Ts' = map (Type.cert_typ tsig) pat_Ts;
-    val is_const = isSome o const_type;
+    val is_const = is_some o const_type;
     val raw_ts' =
       map (decode_types tsig is_const def_type def_sort map_const map_type map_sort) raw_ts;
     val (ts, Ts, unifier) = basic_infer_types pp const_type