avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
authorwenzelm
Fri Dec 15 00:08:06 2006 +0100 (2006-12-15)
changeset 2185805f57309170c
parent 21857 f9d085c2625c
child 21859 03e1e75ad2e5
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
TFL/casesplit.ML
TFL/rules.ML
src/HOL/Import/hol4rews.ML
src/HOL/Import/importrecorder.ML
src/HOL/Import/xmlconv.ML
src/HOL/Matrix/cplex/Cplex_tools.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/ATP/AtpCommunication.ML
src/HOL/Tools/function_package/fundef_lib.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_clause.ML
src/HOL/Tools/res_hol_clause.ML
src/HOL/Tools/sat_solver.ML
src/HOL/Tools/specification_package.ML
src/Pure/General/file.ML
src/Pure/General/name_space.ML
src/Pure/General/path.ML
src/Pure/General/scan.ML
src/Pure/General/symbol.ML
src/Pure/General/url.ML
src/Pure/General/xml.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_output.ML
src/Pure/Isar/outer_lex.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/session.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/ProofGeneral/pgip_output.ML
src/Pure/ProofGeneral/pgip_types.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/ROOT.ML
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Thy/html.ML
src/Pure/Thy/present.ML
src/Pure/Thy/thm_database.ML
src/Pure/Thy/thm_deps.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
src/Pure/Tools/codegen_names.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/codegen.ML
src/Pure/proof_general.ML
src/Pure/type.ML
     1.1 --- a/TFL/casesplit.ML	Thu Dec 14 22:19:39 2006 +0100
     1.2 +++ b/TFL/casesplit.ML	Fri Dec 15 00:08:06 2006 +0100
     1.3 @@ -268,7 +268,7 @@
     1.4  having to (re)search for variables to split. *)
     1.5  fun splitto splitths genth =
     1.6      let
     1.7 -      val _ = assert (not (null splitths)) "splitto: no given splitths";
     1.8 +      val _ = not (null splitths) orelse error "splitto: no given splitths";
     1.9        val sgn = Thm.sign_of_thm genth;
    1.10  
    1.11        (* check if we are a member of splitths - FIXME: quicker and
     2.1 --- a/TFL/rules.ML	Thu Dec 14 22:19:39 2006 +0100
     2.2 +++ b/TFL/rules.ML	Fri Dec 15 00:08:06 2006 +0100
     2.3 @@ -698,9 +698,8 @@
     2.4                    end
     2.5               fun pq_eliminate (thm,sign,vlist,imp_body,lhs_eq) =
     2.6                let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
     2.7 -                  val dummy = assert (forall (op aconv)
     2.8 -                                      (ListPair.zip (vlist, args)))
     2.9 -                               "assertion failed in CONTEXT_REWRITE_RULE"
    2.10 +                  val dummy = forall (op aconv) (ListPair.zip (vlist, args))
    2.11 +                    orelse error "assertion failed in CONTEXT_REWRITE_RULE"
    2.12                    val imp_body1 = subst_free (ListPair.zip (args, vstrl))
    2.13                                               imp_body
    2.14                    val tych = cterm_of sign
     3.1 --- a/src/HOL/Import/hol4rews.ML	Thu Dec 14 22:19:39 2006 +0100
     3.2 +++ b/src/HOL/Import/hol4rews.ML	Fri Dec 15 00:08:06 2006 +0100
     3.3 @@ -584,7 +584,7 @@
     3.4  	    if internal
     3.5  	    then
     3.6  		let
     3.7 -		    val paths = NameSpace.unpack isa
     3.8 +		    val paths = NameSpace.explode isa
     3.9  		    val i = Library.drop(length paths - 2,paths)
    3.10  		in
    3.11  		    case i of
    3.12 @@ -638,10 +638,10 @@
    3.13  
    3.14  	fun gen2replay in_thy out_thy s = 
    3.15  	    let
    3.16 -		val ss = NameSpace.unpack s
    3.17 +		val ss = NameSpace.explode s
    3.18  	    in
    3.19  		if (hd ss = in_thy) then 
    3.20 -		    NameSpace.pack (out_thy::(tl ss))
    3.21 +		    NameSpace.implode (out_thy::(tl ss))
    3.22  		else
    3.23  		    s
    3.24  	    end 
     4.1 --- a/src/HOL/Import/importrecorder.ML	Thu Dec 14 22:19:39 2006 +0100
     4.2 +++ b/src/HOL/Import/importrecorder.ML	Fri Dec 15 00:08:06 2006 +0100
     4.3 @@ -188,7 +188,7 @@
     4.4  fun set_skip_import_dir dir = (history_dir := dir)
     4.5  fun get_skip_import_dir () = !history_dir
     4.6  
     4.7 -fun get_filename thyname = Path.pack (Path.append (Path.unpack (the (get_skip_import_dir ()))) (Path.unpack (thyname^".history")))
     4.8 +fun get_filename thyname = Path.implode (Path.append (Path.explode (the (get_skip_import_dir ()))) (Path.explode (thyname^".history")))
     4.9  
    4.10  fun save_history thyname = 
    4.11      if get_skip_import () then
    4.12 @@ -202,7 +202,7 @@
    4.13  	    val filename = get_filename thyname
    4.14  	    val _ = writeln "load_history / before"
    4.15  	    val _ = 
    4.16 -		if File.exists (Path.unpack filename) then					
    4.17 +		if File.exists (Path.explode filename) then					
    4.18  		    (history := XMLConv.read_from_file history_of_xml (get_filename thyname)) 
    4.19  		else
    4.20  		    clear_history ()
     5.1 --- a/src/HOL/Import/xmlconv.ML	Thu Dec 14 22:19:39 2006 +0100
     5.2 +++ b/src/HOL/Import/xmlconv.ML	Fri Dec 15 00:08:06 2006 +0100
     5.3 @@ -243,12 +243,12 @@
     5.4      ) e
     5.5  
     5.6  
     5.7 -fun to_file f output fname x = File.write (Path.unpack fname) (f (output x))
     5.8 +fun to_file f output fname x = File.write (Path.explode fname) (f (output x))
     5.9   
    5.10  fun from_file f input fname = 
    5.11      let
    5.12  	val _ = writeln "read_from_file enter"
    5.13 -	val s = File.read (Path.unpack fname)
    5.14 +	val s = File.read (Path.explode fname)
    5.15  	val _ = writeln "done: read file"
    5.16  	val tree = timeit (fn () => f s)
    5.17  	val _ = writeln "done: tree"
     6.1 --- a/src/HOL/Matrix/cplex/Cplex_tools.ML	Thu Dec 14 22:19:39 2006 +0100
     6.2 +++ b/src/HOL/Matrix/cplex/Cplex_tools.ML	Fri Dec 15 00:08:06 2006 +0100
     6.3 @@ -1136,7 +1136,7 @@
     6.4  
     6.5  exception Execute of string;
     6.6  
     6.7 -fun tmp_file s = Path.pack (Path.expand (File.tmp_path (Path.make [s])));
     6.8 +fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s])));
     6.9  fun wrap s = "\""^s^"\"";
    6.10  
    6.11  fun solve_glpk prog =
     7.1 --- a/src/HOL/Nominal/nominal_package.ML	Thu Dec 14 22:19:39 2006 +0100
     7.2 +++ b/src/HOL/Nominal/nominal_package.ML	Fri Dec 15 00:08:06 2006 +0100
     7.3 @@ -733,8 +733,8 @@
     7.4  
     7.5      (** strips the "_Rep" in type names *)
     7.6      fun strip_nth_name i s =
     7.7 -      let val xs = NameSpace.unpack s;
     7.8 -      in NameSpace.pack (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
     7.9 +      let val xs = NameSpace.explode s;
    7.10 +      in NameSpace.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
    7.11  
    7.12      val (descr'', ndescr) = ListPair.unzip (List.mapPartial
    7.13        (fn (i, ("Nominal.noption", _, _)) => NONE
     8.1 --- a/src/HOL/Tools/ATP/AtpCommunication.ML	Thu Dec 14 22:19:39 2006 +0100
     8.2 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML	Fri Dec 15 00:08:06 2006 +0100
     8.3 @@ -128,7 +128,8 @@
     8.4  (*Return everything in s that comes before the string t*)
     8.5  fun cut_before t s = 
     8.6    let val (s1,s2) = Substring.position t (Substring.full s)
     8.7 -      val _ = assert (Substring.size s2 <> 0) "cut_before: string not found" 
     8.8 +      val _ = Substring.size s2 <> 0
     8.9 +        orelse error "cut_before: string not found"
    8.10    in Substring.string s2 end;
    8.11  
    8.12  val start_E = "# Proof object starts here."
     9.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML	Thu Dec 14 22:19:39 2006 +0100
     9.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML	Fri Dec 15 00:08:06 2006 +0100
     9.3 @@ -54,7 +54,8 @@
     9.4        val (_, ctx') = ProofContext.add_fixes_i [(n', SOME T, NoSyn)] ctx
     9.5  
     9.6        val (n'', body) = Term.dest_abs (n', T, b) 
     9.7 -      val _ = assert (n' = n'') "dest_all_ctx" (* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *)
     9.8 +      val _ = (n' = n'') orelse error "dest_all_ctx"
     9.9 +      (* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *)
    9.10  
    9.11        val (ctx'', vs, bd) = dest_all_all_ctx ctx' body
    9.12      in
    9.13 @@ -133,4 +134,4 @@
    9.14  
    9.15  
    9.16  
    9.17 -end
    9.18 \ No newline at end of file
    9.19 +end
    10.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Dec 14 22:19:39 2006 +0100
    10.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Fri Dec 15 00:08:06 2006 +0100
    10.3 @@ -296,12 +296,12 @@
    10.4      val (_, params) = strip_comb S;
    10.5      val params' = map dest_Var params;
    10.6      val rss = [] |> fold add_rule intrs;
    10.7 -    val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss)));
    10.8 +    val (prfx, _) = split_last (NameSpace.explode (fst (hd rss)));
    10.9      val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
   10.10  
   10.11      val thy1 = thy |>
   10.12        Theory.root_path |>
   10.13 -      Theory.add_path (NameSpace.pack prfx);
   10.14 +      Theory.add_path (NameSpace.implode prfx);
   10.15      val (ty_eqs, rlz_eqs) = split_list
   10.16        (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs rs) rss);
   10.17  
    11.1 --- a/src/HOL/Tools/record_package.ML	Thu Dec 14 22:19:39 2006 +0100
    11.2 +++ b/src/HOL/Tools/record_package.ML	Fri Dec 15 00:08:06 2006 +0100
    11.3 @@ -439,8 +439,8 @@
    11.4  fun get_extT_fields thy T =
    11.5    let
    11.6      val ((name,Ts),moreT) = dest_recT T;
    11.7 -    val recname = let val (nm::recn::rst) = rev (NameSpace.unpack name)
    11.8 -                  in NameSpace.pack (rev (nm::rst)) end;
    11.9 +    val recname = let val (nm::recn::rst) = rev (NameSpace.explode name)
   11.10 +                  in NameSpace.implode (rev (nm::rst)) end;
   11.11      val midx = maxidx_of_typs (moreT::Ts);
   11.12      val varifyT = varifyT midx;
   11.13      val {records,extfields,...} = RecordsData.get thy;
    12.1 --- a/src/HOL/Tools/res_atp.ML	Thu Dec 14 22:19:39 2006 +0100
    12.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Dec 15 00:08:06 2006 +0100
    12.3 @@ -99,13 +99,13 @@
    12.4        "" => error  ("Isabelle environment variable " ^ evar ^ " not defined")
    12.5      | home =>
    12.6          let val path = home ^ "/" ^ base
    12.7 -        in  if File.exists (File.unpack_platform_path path) then path
    12.8 +        in  if File.exists (File.explode_platform_path path) then path
    12.9              else error ("Could not find the file " ^ path)
   12.10          end;
   12.11  
   12.12  fun probfile_nosuffix _ =
   12.13    if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
   12.14 -  else if File.exists (File.unpack_platform_path (!destdir))
   12.15 +  else if File.exists (File.explode_platform_path (!destdir))
   12.16    then !destdir ^ "/" ^ !problem_name
   12.17    else error ("No such directory: " ^ !destdir);
   12.18  
   12.19 @@ -149,7 +149,7 @@
   12.20      let val file = !problem_name
   12.21      in
   12.22          if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
   12.23 -        else if File.exists (File.unpack_platform_path (!destdir))
   12.24 +        else if File.exists (File.explode_platform_path (!destdir))
   12.25          then !destdir ^ "/" ^ file
   12.26          else error ("No such directory: " ^ !destdir)
   12.27      end;
   12.28 @@ -463,7 +463,7 @@
   12.29  (*Reject theorems with names like "List.filter.filter_list_def" or
   12.30    "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
   12.31  fun is_package_def a =
   12.32 -  let val names = NameSpace.unpack a
   12.33 +  let val names = NameSpace.explode a
   12.34    in
   12.35       length names > 2 andalso
   12.36       not (hd names = "local") andalso
   12.37 @@ -820,7 +820,7 @@
   12.38    end
   12.39  
   12.40  fun trace_array fname =
   12.41 -  let val path = File.unpack_platform_path fname
   12.42 +  let val path = File.explode_platform_path fname
   12.43    in  Array.app (File.append path o (fn s => s ^ "\n"))  end;
   12.44  
   12.45  (*Converting a subgoal into negated conjecture clauses*)
    13.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Dec 14 22:19:39 2006 +0100
    13.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Dec 15 00:08:06 2006 +0100
    13.3 @@ -460,7 +460,7 @@
    13.4    handle THM _ => [];
    13.5  
    13.6  (*Keep the full complexity of the original name*)
    13.7 -fun flatten_name s = space_implode "_X" (NameSpace.unpack s);
    13.8 +fun flatten_name s = space_implode "_X" (NameSpace.explode s);
    13.9  
   13.10  (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
   13.11    It returns a modified theory, unless skolemization fails.*)
    14.1 --- a/src/HOL/Tools/res_clause.ML	Thu Dec 14 22:19:39 2006 +0100
    14.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Dec 15 00:08:06 2006 +0100
    14.3 @@ -745,7 +745,7 @@
    14.4      val clss = conjectures @ axclauses
    14.5      val funcs = funcs_of_clauses clss arity_clauses
    14.6      and preds = preds_of_clauses clss classrel_clauses arity_clauses
    14.7 -    and probname = Path.pack (Path.base (Path.unpack filename))
    14.8 +    and probname = Path.implode (Path.base (Path.explode filename))
    14.9      val (axstrs, _) = ListPair.unzip (map clause2dfg axclauses)
   14.10      val tfree_clss = map dfg_tfree_clause (union_all tfree_litss) 
   14.11      val out = TextIO.openOut filename
    15.1 --- a/src/HOL/Tools/res_hol_clause.ML	Thu Dec 14 22:19:39 2006 +0100
    15.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Fri Dec 15 00:08:06 2006 +0100
    15.3 @@ -578,7 +578,7 @@
    15.4  	val conjectures = make_conjecture_clauses thms
    15.5          val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses)
    15.6  	val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
    15.7 -	and probname = Path.pack (Path.base (Path.unpack filename))
    15.8 +	and probname = Path.implode (Path.base (Path.explode filename))
    15.9  	val axstrs = map (#1 o clause2dfg) axclauses'
   15.10  	val tfree_clss = map ResClause.dfg_tfree_clause (ResClause.union_all tfree_litss)
   15.11  	val out = TextIO.openOut filename
    16.1 --- a/src/HOL/Tools/sat_solver.ML	Thu Dec 14 22:19:39 2006 +0100
    16.2 +++ b/src/HOL/Tools/sat_solver.ML	Fri Dec 15 00:08:06 2006 +0100
    16.3 @@ -564,14 +564,14 @@
    16.4  	fun minisat_with_proofs fm =
    16.5  	let
    16.6  		val _          = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
    16.7 -		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
    16.8 -		val outpath    = File.tmp_path (Path.unpack "result")
    16.9 -		val proofpath  = File.tmp_path (Path.unpack "result.prf")
   16.10 -		val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.pack inpath) ^ " -r " ^ (Path.pack outpath) ^ " -t " ^ (Path.pack proofpath) ^ "> /dev/null"
   16.11 +		val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
   16.12 +		val outpath    = File.tmp_path (Path.explode "result")
   16.13 +		val proofpath  = File.tmp_path (Path.explode "result.prf")
   16.14 +		val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " -t " ^ (Path.implode proofpath) ^ "> /dev/null"
   16.15  		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm
   16.16  		fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
   16.17 -		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
   16.18 -		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
   16.19 +		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
   16.20 +		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
   16.21  		val cnf        = PropLogic.defcnf fm
   16.22  		val result     = SatSolver.make_external_solver cmd writefn readfn cnf
   16.23  		val _          = try File.rm inpath
   16.24 @@ -749,13 +749,13 @@
   16.25  	fun minisat fm =
   16.26  	let
   16.27  		val _          = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
   16.28 -		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
   16.29 -		val outpath    = File.tmp_path (Path.unpack "result")
   16.30 -		val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.pack inpath) ^ " -r " ^ (Path.pack outpath) ^ " > /dev/null"
   16.31 +		val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
   16.32 +		val outpath    = File.tmp_path (Path.explode "result")
   16.33 +		val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " > /dev/null"
   16.34  		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   16.35  		fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
   16.36 -		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
   16.37 -		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
   16.38 +		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
   16.39 +		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
   16.40  		val result     = SatSolver.make_external_solver cmd writefn readfn fm
   16.41  		val _          = try File.rm inpath
   16.42  		val _          = try File.rm outpath
   16.43 @@ -788,7 +788,7 @@
   16.44  	  SatSolver.UNSATISFIABLE NONE =>
   16.45  		(let
   16.46  			(* string list *)
   16.47 -			val proof_lines = ((split_lines o File.read) (Path.unpack "resolve_trace"))
   16.48 +			val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace"))
   16.49  				handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
   16.50  			(* PropLogic.prop_formula -> int *)
   16.51  			fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
   16.52 @@ -911,13 +911,13 @@
   16.53  		                    (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
   16.54  			(* both versions of zChaff appear to have the same interface, so we do *)
   16.55  			(* not actually need to distinguish between them in the following code *)
   16.56 -		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
   16.57 -		val outpath    = File.tmp_path (Path.unpack "result")
   16.58 -		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
   16.59 +		val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
   16.60 +		val outpath    = File.tmp_path (Path.explode "result")
   16.61 +		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
   16.62  		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   16.63  		fun readfn ()  = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
   16.64 -		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
   16.65 -		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
   16.66 +		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
   16.67 +		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
   16.68  		val result     = SatSolver.make_external_solver cmd writefn readfn fm
   16.69  		val _          = try File.rm inpath
   16.70  		val _          = try File.rm outpath
   16.71 @@ -936,13 +936,13 @@
   16.72  	fun berkmin fm =
   16.73  	let
   16.74  		val _          = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else ()
   16.75 -		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
   16.76 -		val outpath    = File.tmp_path (Path.unpack "result")
   16.77 -		val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
   16.78 +		val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
   16.79 +		val outpath    = File.tmp_path (Path.explode "result")
   16.80 +		val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
   16.81  		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   16.82  		fun readfn ()  = SatSolver.read_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
   16.83 -		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
   16.84 -		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
   16.85 +		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
   16.86 +		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
   16.87  		val result     = SatSolver.make_external_solver cmd writefn readfn fm
   16.88  		val _          = try File.rm inpath
   16.89  		val _          = try File.rm outpath
   16.90 @@ -961,13 +961,13 @@
   16.91  	fun jerusat fm =
   16.92  	let
   16.93  		val _          = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
   16.94 -		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
   16.95 -		val outpath    = File.tmp_path (Path.unpack "result")
   16.96 -		val cmd        = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
   16.97 +		val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
   16.98 +		val outpath    = File.tmp_path (Path.explode "result")
   16.99 +		val cmd        = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
  16.100  		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
  16.101  		fun readfn ()  = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
  16.102 -		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
  16.103 -		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
  16.104 +		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
  16.105 +		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
  16.106  		val result     = SatSolver.make_external_solver cmd writefn readfn fm
  16.107  		val _          = try File.rm inpath
  16.108  		val _          = try File.rm outpath
    17.1 --- a/src/HOL/Tools/specification_package.ML	Thu Dec 14 22:19:39 2006 +0100
    17.2 +++ b/src/HOL/Tools/specification_package.ML	Fri Dec 15 00:08:06 2006 +0100
    17.3 @@ -128,8 +128,8 @@
    17.4          fun proc_single prop =
    17.5              let
    17.6                  val frees = Term.term_frees prop
    17.7 -                val _ = assert (forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees)
    17.8 -                               "Specificaton: Only free variables of sort 'type' allowed"
    17.9 +                val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
   17.10 +                  orelse error "Specificaton: Only free variables of sort 'type' allowed"
   17.11                  val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees)
   17.12              in
   17.13                  (prop_closed,frees)
   17.14 @@ -145,8 +145,8 @@
   17.15          val (altcos,overloaded) = Library.split_list cos
   17.16          val (names,sconsts) = Library.split_list altcos
   17.17          val consts = map (term_of o Thm.read_cterm thy o rpair TypeInfer.logicT) sconsts
   17.18 -        val _ = assert (not (Library.exists (not o Term.is_Const) consts))
   17.19 -                       "Specification: Non-constant found as parameter"
   17.20 +        val _ = not (Library.exists (not o Term.is_Const) consts)
   17.21 +          orelse error "Specification: Non-constant found as parameter"
   17.22  
   17.23          fun proc_const c =
   17.24              let
    18.1 --- a/src/Pure/General/file.ML	Thu Dec 14 22:19:39 2006 +0100
    18.2 +++ b/src/Pure/General/file.ML	Fri Dec 15 00:08:06 2006 +0100
    18.3 @@ -7,8 +7,8 @@
    18.4  
    18.5  signature FILE =
    18.6  sig
    18.7 -  val unpack_platform_path_fn: (string -> Path.T) ref
    18.8 -  val unpack_platform_path: string -> Path.T
    18.9 +  val explode_platform_path_fn: (string -> Path.T) ref
   18.10 +  val explode_platform_path: string -> Path.T
   18.11    val platform_path_fn: (Path.T -> string) ref
   18.12    val platform_path: Path.T -> string
   18.13    val shell_path_fn: (Path.T -> string) ref
   18.14 @@ -22,7 +22,7 @@
   18.15    eqtype info
   18.16    val info: Path.T -> info option
   18.17    val exists: Path.T -> bool
   18.18 -  val assert: Path.T -> unit
   18.19 +  val check: Path.T -> unit
   18.20    val rm: Path.T -> unit
   18.21    val mkdir: Path.T -> unit
   18.22    val read: Path.T -> string
   18.23 @@ -41,20 +41,20 @@
   18.24  
   18.25  (* platform specific path representations *)
   18.26  
   18.27 -val unpack_platform_path_fn = ref Path.unpack;
   18.28 -fun unpack_platform_path s = ! unpack_platform_path_fn s;
   18.29 +val explode_platform_path_fn = ref Path.explode;
   18.30 +fun explode_platform_path s = ! explode_platform_path_fn s;
   18.31  
   18.32 -val platform_path_fn = ref (Path.pack o Path.expand);
   18.33 +val platform_path_fn = ref (Path.implode o Path.expand);
   18.34  fun platform_path path = ! platform_path_fn path;
   18.35  
   18.36 -val shell_path_fn = ref (enclose "'" "'" o Path.pack o Path.expand);
   18.37 +val shell_path_fn = ref (enclose "'" "'" o Path.implode o Path.expand);
   18.38  fun shell_path path = ! shell_path_fn path;
   18.39  
   18.40  
   18.41  (* current path *)
   18.42  
   18.43  val cd = Library.cd o platform_path;
   18.44 -val pwd = unpack_platform_path o Library.pwd;
   18.45 +val pwd = explode_platform_path o Library.pwd;
   18.46  
   18.47  fun norm_absolute p =
   18.48    let
   18.49 @@ -94,9 +94,9 @@
   18.50  
   18.51  val exists = is_some o info;
   18.52  
   18.53 -fun assert path =
   18.54 +fun check path =
   18.55    if exists path then ()
   18.56 -  else error ("No such file or directory: " ^ quote (Path.pack path));
   18.57 +  else error ("No such file or directory: " ^ quote (Path.implode path));
   18.58  
   18.59  val rm = OS.FileSys.remove o platform_path;
   18.60  
   18.61 @@ -137,12 +137,12 @@
   18.62      SOME ids => OS.FileSys.compare ids = EQUAL
   18.63    | NONE => false);
   18.64  
   18.65 -fun copy from to = conditional (not (eq (from, to))) (fn () =>
   18.66 -  let val target = if is_dir to then Path.append to (Path.base from) else to
   18.67 -  in write target (read from) end);
   18.68 +fun copy src dst = conditional (not (eq (src, dst))) (fn () =>
   18.69 +  let val target = if is_dir dst then Path.append dst (Path.base src) else dst
   18.70 +  in write target (read src) end);
   18.71  
   18.72 -fun copy_dir from to = conditional (not (eq (from, to))) (fn () =>
   18.73 -  (system_command ("cp -r -f " ^ shell_path from ^ "/. " ^ shell_path to); ()))
   18.74 +fun copy_dir src dst = conditional (not (eq (src, dst))) (fn () =>
   18.75 +  (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ()))
   18.76  
   18.77  
   18.78  (* use ML files *)
    19.1 --- a/src/Pure/General/name_space.ML	Thu Dec 14 22:19:39 2006 +0100
    19.2 +++ b/src/Pure/General/name_space.ML	Fri Dec 15 00:08:06 2006 +0100
    19.3 @@ -22,8 +22,8 @@
    19.4    val hidden: string -> string
    19.5    val separator: string                 (*single char*)
    19.6    val is_qualified: string -> bool
    19.7 -  val pack: string list -> string
    19.8 -  val unpack: string -> string list
    19.9 +  val implode: string list -> string
   19.10 +  val explode: string -> string list
   19.11    val append: string -> string -> string
   19.12    val qualified: string -> string -> string
   19.13    val base: string -> string
   19.14 @@ -70,8 +70,8 @@
   19.15  val separator = ".";
   19.16  val is_qualified = exists_string (fn s => s = separator);
   19.17  
   19.18 -val pack = space_implode separator;
   19.19 -val unpack = space_explode separator;
   19.20 +val implode_name = space_implode separator;
   19.21 +val explode_name = space_explode separator;
   19.22  
   19.23  fun append name1 "" = name1
   19.24    | append "" name2 = name2
   19.25 @@ -82,15 +82,15 @@
   19.26    else path ^ separator ^ name;
   19.27  
   19.28  fun base "" = ""
   19.29 -  | base name = List.last (unpack name);
   19.30 +  | base name = List.last (explode_name name);
   19.31  
   19.32  fun qualifier "" = ""
   19.33 -  | qualifier name = pack (#1 (split_last (unpack name)));
   19.34 +  | qualifier name = implode_name (#1 (split_last (explode_name name)));
   19.35  
   19.36  fun map_base _ "" = ""
   19.37    | map_base f name =
   19.38 -      let val names = unpack name
   19.39 -      in pack (nth_map (length names - 1) f names) end;
   19.40 +      let val names = explode_name name
   19.41 +      in implode_name (nth_map (length names - 1) f names) end;
   19.42  
   19.43  
   19.44  (* accesses *)
   19.45 @@ -117,8 +117,8 @@
   19.46        [xs @ ys] @@ prefixes1 zs @@ [ws];
   19.47    in sfxs @ pfxs end;
   19.48  
   19.49 -val accesses = map pack o suffixes_prefixes o unpack;
   19.50 -val accesses' = map pack o Library.suffixes1 o unpack;
   19.51 +val accesses = map implode_name o suffixes_prefixes o explode_name;
   19.52 +val accesses' = map implode_name o Library.suffixes1 o explode_name;
   19.53  
   19.54  
   19.55  
   19.56 @@ -228,10 +228,10 @@
   19.57    if is_hidden name then
   19.58      error ("Attempt to declare hidden name " ^ quote name)
   19.59    else
   19.60 -    let val names = unpack name in
   19.61 +    let val names = explode_name name in
   19.62        conditional (null names orelse exists (fn s => s = "") names) (fn () =>
   19.63          error ("Bad name declaration " ^ quote name));
   19.64 -      fold (add_name name) (map pack (accs names)) space
   19.65 +      fold (add_name name) (map implode_name (accs names)) space
   19.66      end;
   19.67  
   19.68  
   19.69 @@ -258,7 +258,7 @@
   19.70  
   19.71  fun sticky_prefix prfx (Naming (path, (qualify, _))) =
   19.72    Naming (append path prfx,
   19.73 -    (qualify, suffixes_prefixes_split (length (unpack path)) (length (unpack prfx))));
   19.74 +    (qualify, suffixes_prefixes_split (length (explode_name path)) (length (explode_name prfx))));
   19.75  
   19.76  fun set_policy policy (Naming (path, _)) = Naming (path, policy);
   19.77  
   19.78 @@ -284,6 +284,11 @@
   19.79  fun dest_table tab = map (apfst #1) (ext_table tab);
   19.80  fun extern_table tab = map (apfst #2) (ext_table tab);
   19.81  
   19.82 +
   19.83 +(*final declarations of this structure!*)
   19.84 +val implode = implode_name;
   19.85 +val explode = explode_name;
   19.86 +
   19.87  end;
   19.88  
   19.89  structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
    20.1 --- a/src/Pure/General/path.ML	Thu Dec 14 22:19:39 2006 +0100
    20.2 +++ b/src/Pure/General/path.ML	Fri Dec 15 00:08:06 2006 +0100
    20.3 @@ -21,8 +21,8 @@
    20.4    val append: T -> T -> T
    20.5    val appends: T list -> T
    20.6    val make: string list -> T
    20.7 -  val pack: T -> string
    20.8 -  val unpack: string -> T
    20.9 +  val implode: T -> string
   20.10 +  val explode: string -> T
   20.11    val dir: T -> T
   20.12    val base: T -> T
   20.13    val ext: string -> T -> T
   20.14 @@ -95,35 +95,35 @@
   20.15  fun norm path = rev_app [] path;
   20.16  
   20.17  
   20.18 -(* pack *)
   20.19 +(* implode *)
   20.20  
   20.21 -fun pack_elem Root = ""
   20.22 -  | pack_elem Parent = ".."
   20.23 -  | pack_elem (Basic s) = s
   20.24 -  | pack_elem (Variable s) = "$" ^ s;
   20.25 +fun implode_elem Root = ""
   20.26 +  | implode_elem Parent = ".."
   20.27 +  | implode_elem (Basic s) = s
   20.28 +  | implode_elem (Variable s) = "$" ^ s;
   20.29  
   20.30 -fun pack (Path []) = "."
   20.31 -  | pack (Path (Root :: xs)) = "/" ^ space_implode "/" (map pack_elem xs)
   20.32 -  | pack (Path xs) = space_implode "/" (map pack_elem xs);
   20.33 +fun implode_path (Path []) = "."
   20.34 +  | implode_path (Path (Root :: xs)) = "/" ^ space_implode "/" (map implode_elem xs)
   20.35 +  | implode_path (Path xs) = space_implode "/" (map implode_elem xs);
   20.36  
   20.37  
   20.38 -(* unpack *)
   20.39 +(* explode *)
   20.40  
   20.41 -fun unpack_elem "" = Root
   20.42 -  | unpack_elem ".." = Parent
   20.43 -  | unpack_elem "~" = Variable "HOME"
   20.44 -  | unpack_elem "~~" = Variable "ISABELLE_HOME"
   20.45 -  | unpack_elem s =
   20.46 +fun explode_elem "" = Root
   20.47 +  | explode_elem ".." = Parent
   20.48 +  | explode_elem "~" = Variable "HOME"
   20.49 +  | explode_elem "~~" = Variable "ISABELLE_HOME"
   20.50 +  | explode_elem s =
   20.51        (case explode s of
   20.52          "$" :: cs => variable_elem cs
   20.53        | cs => basic_elem cs);
   20.54  
   20.55 -val unpack_elems = map unpack_elem o filter_out (fn c => c = "" orelse c = ".");
   20.56 +val explode_elems = map explode_elem o filter_out (fn c => c = "" orelse c = ".");
   20.57  
   20.58 -fun unpack str = Path (norm
   20.59 +fun explode_path str = Path (norm
   20.60    (case space_explode "/" str of
   20.61 -    "" :: ss => Root :: unpack_elems ss
   20.62 -  | ss => unpack_elems ss));
   20.63 +    "" :: ss => Root :: explode_elems ss
   20.64 +  | ss => explode_elems ss));
   20.65  
   20.66  
   20.67  (* base element *)
   20.68 @@ -131,7 +131,7 @@
   20.69  fun split_path f (path as Path xs) =
   20.70    (case try split_last xs of
   20.71      SOME (prfx, Basic s) => f (prfx, s)
   20.72 -  | _ => error ("Cannot split path into dir/base: " ^ quote (pack path)));
   20.73 +  | _ => error ("Cannot split path into dir/base: " ^ quote (implode_path path)));
   20.74  
   20.75  val dir = split_path (fn (prfx, _) => Path prfx);
   20.76  val base = split_path (fn (_, s) => Path [Basic s]);
   20.77 @@ -150,10 +150,15 @@
   20.78  fun eval (Variable s) =
   20.79      (case getenv s of
   20.80        "" => error ("Undefined Isabelle environment variable: " ^ quote s)
   20.81 -    | path => rep (unpack path))
   20.82 +    | path => rep (explode_path path))
   20.83    | eval x = [x];
   20.84  
   20.85  val expand = rep #> maps eval #> norm #> Path;
   20.86 -val position = expand #> pack #> quote #> Position.line_name 1;
   20.87 +val position = expand #> implode_path #> quote #> Position.line_name 1;
   20.88 +
   20.89 +
   20.90 +(*final declarations of this structure!*)
   20.91 +val implode = implode_path;
   20.92 +val explode = explode_path;
   20.93  
   20.94  end;
    21.1 --- a/src/Pure/General/scan.ML	Thu Dec 14 22:19:39 2006 +0100
    21.2 +++ b/src/Pure/General/scan.ML	Fri Dec 15 00:08:06 2006 +0100
    21.3 @@ -42,8 +42,8 @@
    21.4    val one: ('a -> bool) -> 'a list -> 'a * 'a list
    21.5    val this: string list -> string list -> string list * string list
    21.6    val this_string: string -> string list -> string * string list
    21.7 -  val any: ('a -> bool) -> 'a list -> 'a list * 'a list
    21.8 -  val any1: ('a -> bool) -> 'a list -> 'a list * 'a list
    21.9 +  val many: ('a -> bool) -> 'a list -> 'a list * 'a list
   21.10 +  val many1: ('a -> bool) -> 'a list -> 'a list * 'a list
   21.11    val optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a
   21.12    val option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
   21.13    val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
   21.14 @@ -143,12 +143,12 @@
   21.15  
   21.16  fun this_string s = this (explode s) >> K s;  (*primitive string -- no symbols here!*)
   21.17  
   21.18 -fun any _ [] = raise MORE NONE
   21.19 -  | any pred (lst as x :: xs) =
   21.20 -      if pred x then apfst (cons x) (any pred xs)
   21.21 +fun many _ [] = raise MORE NONE
   21.22 +  | many pred (lst as x :: xs) =
   21.23 +      if pred x then apfst (cons x) (many pred xs)
   21.24        else ([], lst);
   21.25  
   21.26 -fun any1 pred = one pred -- any pred >> op ::;
   21.27 +fun many1 pred = one pred -- many pred >> op ::;
   21.28  
   21.29  fun optional scan def = scan || succeed def;
   21.30  fun option scan = (scan >> SOME) || succeed NONE;
    22.1 --- a/src/Pure/General/symbol.ML	Thu Dec 14 22:19:39 2006 +0100
    22.2 +++ b/src/Pure/General/symbol.ML	Fri Dec 15 00:08:06 2006 +0100
    22.3 @@ -403,7 +403,7 @@
    22.4  
    22.5  (* scan *)
    22.6  
    22.7 -val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode);
    22.8 +val scan_id = Scan.one is_letter ^^ (Scan.many is_letdig >> implode);
    22.9  
   22.10  local
   22.11  
   22.12 @@ -413,8 +413,8 @@
   22.13    $$ "\\" -- Scan.optional ($$ "\\") "" -- Scan.this_string "<^newline>" >> K "\n";
   22.14  
   22.15  val scan_raw =
   22.16 -  Scan.this_string "raw:" ^^ (Scan.any raw_chr >> implode) ||
   22.17 -  Scan.this_string "raw" ^^ (Scan.any1 is_ascii_digit >> implode);
   22.18 +  Scan.this_string "raw:" ^^ (Scan.many raw_chr >> implode) ||
   22.19 +  Scan.this_string "raw" ^^ (Scan.many1 is_ascii_digit >> implode);
   22.20  
   22.21  in
   22.22  
   22.23 @@ -431,7 +431,7 @@
   22.24  (* source *)
   22.25  
   22.26  val recover =
   22.27 -  Scan.any (fn s => not (is_blank s) andalso s <> "\"" andalso not_eof s) >> K [malformed];
   22.28 +  Scan.many (fn s => not (is_blank s) andalso s <> "\"" andalso not_eof s) >> K [malformed];
   22.29  
   22.30  fun source do_recover src =
   22.31    Source.source stopper (Scan.bulk scan) (if do_recover then SOME recover else NONE) src;
    23.1 --- a/src/Pure/General/url.ML	Thu Dec 14 22:19:39 2006 +0100
    23.2 +++ b/src/Pure/General/url.ML	Fri Dec 15 00:08:06 2006 +0100
    23.3 @@ -13,8 +13,8 @@
    23.4      Http of string * Path.T |
    23.5      Ftp of string * Path.T
    23.6    val append: T -> T -> T
    23.7 -  val pack: T -> string
    23.8 -  val unpack: string -> T
    23.9 +  val implode: T -> string
   23.10 +  val explode: string -> T
   23.11  end;
   23.12  
   23.13  structure Url: URL =
   23.14 @@ -38,26 +38,26 @@
   23.15    | append _ url = url;
   23.16  
   23.17  
   23.18 -(* pack *)
   23.19 +(* implode *)
   23.20  
   23.21 -fun pack_path p = if Path.is_current p then "" else Path.pack p;
   23.22 +fun implode_path p = if Path.is_current p then "" else Path.implode p;
   23.23  
   23.24 -fun pack (File p) = pack_path p
   23.25 -  | pack (RemoteFile (h, p)) = "file://" ^ h ^ pack_path p
   23.26 -  | pack (Http (h, p)) = "http://" ^ h ^ pack_path p
   23.27 -  | pack (Ftp (h, p)) = "ftp://" ^ h ^ pack_path p;
   23.28 +fun implode_url (File p) = implode_path p
   23.29 +  | implode_url (RemoteFile (h, p)) = "file://" ^ h ^ implode_path p
   23.30 +  | implode_url (Http (h, p)) = "http://" ^ h ^ implode_path p
   23.31 +  | implode_url (Ftp (h, p)) = "ftp://" ^ h ^ implode_path p;
   23.32  
   23.33  
   23.34 -(* unpack *)
   23.35 +(* explode *)
   23.36  
   23.37  local
   23.38  
   23.39  val scan_host =
   23.40 -  (Scan.any1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
   23.41 +  (Scan.many1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
   23.42    Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
   23.43  
   23.44 -val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
   23.45 -val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o implode o cons "/");
   23.46 +val scan_path = Scan.many Symbol.not_eof >> (Path.explode o implode);
   23.47 +val scan_path_root = Scan.many Symbol.not_eof >> (Path.explode o implode o cons "/");
   23.48  
   23.49  val scan_url =
   23.50    Scan.unless (Scan.this_string "file:" ||
   23.51 @@ -71,8 +71,13 @@
   23.52  
   23.53  in
   23.54  
   23.55 -fun unpack s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
   23.56 +fun explode_url s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
   23.57  
   23.58  end;
   23.59  
   23.60 +
   23.61 +(*final declarations of this structure!*)
   23.62 +val implode = implode_url;
   23.63 +val explode = explode_url;
   23.64 +
   23.65  end;
    24.1 --- a/src/Pure/General/xml.ML	Thu Dec 14 22:19:39 2006 +0100
    24.2 +++ b/src/Pure/General/xml.ML	Fri Dec 15 00:08:06 2006 +0100
    24.3 @@ -118,7 +118,7 @@
    24.4  fun err s (xs, _) =
    24.5    "XML parsing error: " ^ s ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
    24.6  
    24.7 -val scan_whspc = Scan.any Symbol.is_blank;
    24.8 +val scan_whspc = Scan.many Symbol.is_blank;
    24.9  
   24.10  val scan_special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
   24.11  
    25.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Dec 14 22:19:39 2006 +0100
    25.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Dec 15 00:08:06 2006 +0100
    25.3 @@ -192,7 +192,7 @@
    25.4  (* init and exit *)
    25.5  
    25.6  fun begin_theory name imports uses =
    25.7 -  ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.unpack) uses);
    25.8 +  ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.explode) uses);
    25.9  
   25.10  fun end_theory thy =
   25.11    if ThyInfo.check_known_thy (Context.theory_name thy) then ThyInfo.end_theory thy else thy;
   25.12 @@ -298,7 +298,7 @@
   25.13  (* current working directory *)
   25.14  
   25.15  fun cd path = Toplevel.imperative (fn () => (File.cd path));
   25.16 -val pwd = Toplevel.imperative (fn () => writeln (Path.pack (File.pwd ())));
   25.17 +val pwd = Toplevel.imperative (fn () => writeln (Path.implode (File.pwd ())));
   25.18  
   25.19  
   25.20  (* load theory files *)
   25.21 @@ -496,7 +496,7 @@
   25.22  (* markup commands *)
   25.23  
   25.24  fun add_header s = Toplevel.keep' (fn int => fn state =>
   25.25 -  (Toplevel.assert (Toplevel.is_toplevel state);
   25.26 +  (if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF;
   25.27     if int then OuterSyntax.check_text s NONE else ()));
   25.28  
   25.29  local
    26.1 --- a/src/Pure/Isar/isar_output.ML	Thu Dec 14 22:19:39 2006 +0100
    26.2 +++ b/src/Pure/Isar/isar_output.ML	Fri Dec 15 00:08:06 2006 +0100
    26.3 @@ -305,10 +305,10 @@
    26.4  local
    26.5  
    26.6  val space_proper =
    26.7 -  Scan.one T.is_blank -- Scan.any T.is_comment -- Scan.one T.is_proper;
    26.8 +  Scan.one T.is_blank -- Scan.many T.is_comment -- Scan.one T.is_proper;
    26.9  
   26.10  val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore);
   26.11 -val improper = Scan.any is_improper;
   26.12 +val improper = Scan.many is_improper;
   26.13  val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
   26.14  val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one T.is_blank));
   26.15  
   26.16 @@ -375,7 +375,7 @@
   26.17      val cmd = Scan.one (is_some o fst);
   26.18      val non_cmd = Scan.one (is_none o fst andf not o #2 stopper) >> #2;
   26.19  
   26.20 -    val comments = Scan.any (comment_token o fst o snd);
   26.21 +    val comments = Scan.many (comment_token o fst o snd);
   26.22      val blank = Scan.one (blank_token o fst o snd);
   26.23      val newline = Scan.one (newline_token o fst o snd);
   26.24      val before_cmd =
    27.1 --- a/src/Pure/Isar/outer_lex.ML	Thu Dec 14 22:19:39 2006 +0100
    27.2 +++ b/src/Pure/Isar/outer_lex.ML	Fri Dec 15 00:08:06 2006 +0100
    27.3 @@ -193,7 +193,7 @@
    27.4  val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
    27.5  
    27.6  val scan_symid =
    27.7 -  Scan.any1 is_sym_char >> implode ||
    27.8 +  Scan.many1 is_sym_char >> implode ||
    27.9    Scan.one Symbol.is_symbolic;
   27.10  
   27.11  fun is_symid str =
   27.12 @@ -249,8 +249,8 @@
   27.13  fun is_space s = Symbol.is_blank s andalso s <> "\n";
   27.14  
   27.15  val scan_space =
   27.16 -  (keep_line (Scan.any1 is_space) -- Scan.optional (incr_line ($$ "\n")) "" ||
   27.17 -    keep_line (Scan.any is_space) -- incr_line ($$ "\n")) >> (fn (cs, c) => implode cs ^ c);
   27.18 +  (keep_line (Scan.many1 is_space) -- Scan.optional (incr_line ($$ "\n")) "" ||
   27.19 +    keep_line (Scan.many is_space) -- incr_line ($$ "\n")) >> (fn (cs, c) => implode cs ^ c);
   27.20  
   27.21  
   27.22  (* scan nested comments *)
   27.23 @@ -303,7 +303,7 @@
   27.24  (* token sources *)
   27.25  
   27.26  val is_junk = (not o Symbol.is_blank) andf Symbol.not_sync andf Symbol.not_eof;
   27.27 -fun recover xs = (keep_line (Scan.any is_junk) >> (fn ts => [malformed_of ts])) xs;
   27.28 +fun recover xs = (keep_line (Scan.many is_junk) >> (fn ts => [malformed_of ts])) xs;
   27.29  
   27.30  fun source do_recover get_lex pos src =
   27.31    Source.source' pos Symbol.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
    28.1 --- a/src/Pure/Isar/outer_parse.ML	Thu Dec 14 22:19:39 2006 +0100
    28.2 +++ b/src/Pure/Isar/outer_parse.ML	Fri Dec 15 00:08:06 2006 +0100
    28.3 @@ -220,7 +220,7 @@
    28.4  val name = group "name declaration" (short_ident || sym_ident || string || number);
    28.5  val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
    28.6  val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
    28.7 -val path = group "file name/path specification" name >> Path.unpack;
    28.8 +val path = group "file name/path specification" name >> Path.explode;
    28.9  
   28.10  val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
   28.11  
    29.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Dec 14 22:19:39 2006 +0100
    29.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Dec 15 00:08:06 2006 +0100
    29.3 @@ -253,9 +253,9 @@
    29.4      val ml_file = if ml andalso is_some (ThyLoad.check_file NONE ml_path) then [ml_path] else [];
    29.5    in
    29.6      if name <> name' then
    29.7 -      error ("Filename " ^ quote (Path.pack path) ^
    29.8 +      error ("Filename " ^ quote (Path.implode path) ^
    29.9          " does not agree with theory name " ^ quote name')
   29.10 -    else (parents, map (Path.unpack o #1) files @ ml_file)
   29.11 +    else (parents, map (Path.explode o #1) files @ ml_file)
   29.12    end;
   29.13  
   29.14  
   29.15 @@ -268,7 +268,7 @@
   29.16      if is_none (ThyLoad.check_file NONE path) then ()
   29.17      else
   29.18        let
   29.19 -        val _ = warning ("Loading legacy ML script " ^ quote (Path.pack path));
   29.20 +        val _ = warning ("Loading legacy ML script " ^ quote (Path.implode path));
   29.21          val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
   29.22          val tr_name = if time then "time_use" else "use";
   29.23        in Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] end
    30.1 --- a/src/Pure/Isar/session.ML	Thu Dec 14 22:19:39 2006 +0100
    30.2 +++ b/src/Pure/Isar/session.ML	Fri Dec 15 00:08:06 2006 +0100
    30.3 @@ -71,11 +71,11 @@
    30.4       if is_some (! remote_path) then
    30.5         error "Path for remote theory browsing information may only be set once"
    30.6       else
    30.7 -       remote_path := SOME (Url.unpack rpath);
    30.8 +       remote_path := SOME (Url.explode rpath);
    30.9     (! remote_path, rpath <> ""));
   30.10  
   30.11  fun dumping (_, "") = NONE
   30.12 -  | dumping (cp, path) = SOME (cp, Path.unpack path);
   30.13 +  | dumping (cp, path) = SOME (cp, Path.explode path);
   30.14  
   30.15  fun use_dir root build modes reset info doc doc_graph doc_versions
   30.16      parent name dump rpath level verbose =
    31.1 --- a/src/Pure/Proof/extraction.ML	Thu Dec 14 22:19:39 2006 +0100
    31.2 +++ b/src/Pure/Proof/extraction.ML	Fri Dec 15 00:08:06 2006 +0100
    31.3 @@ -315,7 +315,7 @@
    31.4    in fn (thm, (vs, s1, s2)) =>
    31.5      let
    31.6        val name = Thm.get_name thm;
    31.7 -      val _ = assert (name <> "") "add_realizers: unnamed theorem";
    31.8 +      val _ = name <> "" orelse error "add_realizers: unnamed theorem";
    31.9        val prop = Pattern.rewrite_term thy'
   31.10          (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
   31.11        val vars = vars_of prop;
   31.12 @@ -360,7 +360,7 @@
   31.13        defs, expand, prep} = ExtractionData.get thy;
   31.14  
   31.15      val name = Thm.get_name thm;
   31.16 -    val _ = assert (name <> "") "add_expand_thms: unnamed theorem";
   31.17 +    val _ = name <> "" orelse error "add_expand_thms: unnamed theorem";
   31.18  
   31.19      val is_def =
   31.20        (case strip_comb (fst (Logic.dest_equals (prop_of thm))) of
   31.21 @@ -568,7 +568,7 @@
   31.22                NONE => (case find vs' (find' name defs') of
   31.23                  NONE =>
   31.24                    let
   31.25 -                    val _ = assert (T = nullT) "corr: internal error";
   31.26 +                    val _ = T = nullT orelse error "corr: internal error";
   31.27                      val _ = msg d ("Building correctness proof for " ^ quote name ^
   31.28                        (if null vs' then ""
   31.29                         else " (relevant variables: " ^ commas_quote vs' ^ ")"));
   31.30 @@ -720,8 +720,8 @@
   31.31        let
   31.32          val {prop, der = (_, prf), sign, ...} = rep_thm thm;
   31.33          val name = Thm.get_name thm;
   31.34 -        val _ = assert (name <> "") "extraction: unnamed theorem";
   31.35 -        val _ = assert (etype_of thy' vs [] prop <> nullT) ("theorem " ^
   31.36 +        val _ = name <> "" orelse error "extraction: unnamed theorem";
   31.37 +        val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
   31.38            quote name ^ " has no computational content")
   31.39        in (Reconstruct.reconstruct_proof sign prop prf, vs) end;
   31.40  
    32.1 --- a/src/Pure/Proof/proof_syntax.ML	Thu Dec 14 22:19:39 2006 +0100
    32.2 +++ b/src/Pure/Proof/proof_syntax.ML	Fri Dec 15 00:08:06 2006 +0100
    32.3 @@ -134,16 +134,16 @@
    32.4      fun prf_of [] (Bound i) = PBound i
    32.5        | prf_of Ts (Const (s, Type ("proof", _))) =
    32.6            change_type (if ty then SOME Ts else NONE)
    32.7 -            (case NameSpace.unpack s of
    32.8 +            (case NameSpace.explode s of
    32.9                 "axm" :: xs =>
   32.10                   let
   32.11 -                   val name = NameSpace.pack xs;
   32.12 +                   val name = NameSpace.implode xs;
   32.13                     val prop = (case AList.lookup (op =) axms name of
   32.14                         SOME prop => prop
   32.15                       | NONE => error ("Unknown axiom " ^ quote name))
   32.16                   in PAxm (name, prop, NONE) end
   32.17               | "thm" :: xs =>
   32.18 -                 let val name = NameSpace.pack xs;
   32.19 +                 let val name = NameSpace.implode xs;
   32.20                   in (case AList.lookup (op =) thms name of
   32.21                       SOME thm => fst (strip_combt (Thm.proof_of thm))
   32.22                     | NONE => (case Symtab.lookup tab name of
    33.1 --- a/src/Pure/ProofGeneral/pgip_output.ML	Thu Dec 14 22:19:39 2006 +0100
    33.2 +++ b/src/Pure/ProofGeneral/pgip_output.ML	Fri Dec 15 00:08:06 2006 +0100
    33.3 @@ -184,7 +184,7 @@
    33.4                    ("version", version),
    33.5                    ("instance", instance), 
    33.6                    ("descr", descr),
    33.7 -                  ("url", Url.pack url),
    33.8 +                  ("url", Url.implode url),
    33.9                    ("filenameextns", filenameextns)],
   33.10                   [])
   33.11      end
    34.1 --- a/src/Pure/ProofGeneral/pgip_types.ML	Thu Dec 14 22:19:39 2006 +0100
    34.2 +++ b/src/Pure/ProofGeneral/pgip_types.ML	Fri Dec 15 00:08:06 2006 +0100
    34.3 @@ -279,7 +279,7 @@
    34.4  (** Url operations **)
    34.5  
    34.6  fun pgipurl_of_string url = (* only handle file:/// or file://localhost/ *)
    34.7 -	case Url.unpack url of
    34.8 +	case Url.explode url of
    34.9              (Url.File path) => path
   34.10  	  | _ => raise PGIP ("Cannot access non-local URL " ^ url)
   34.11  		       
   34.12 @@ -291,7 +291,7 @@
   34.13  val pgipurl_of_attrs = pgipurl_of_string o (get_attr "url")
   34.14  
   34.15  fun pgipurl_of_url (Url.File p) = p
   34.16 -  | pgipurl_of_url url = raise PGIP ("Cannot access non-local/non-file URL " ^ (Url.pack url))
   34.17 +  | pgipurl_of_url url = raise PGIP ("Cannot access non-local/non-file URL " ^ (Url.implode url))
   34.18  
   34.19  
   34.20  (** Messages and errors **)
    35.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Dec 14 22:19:39 2006 +0100
    35.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Dec 15 00:08:06 2006 +0100
    35.3 @@ -176,7 +176,7 @@
    35.4  
    35.5  (* prepare theory context *)
    35.6  
    35.7 -val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
    35.8 +val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
    35.9  
   35.10  (* FIXME general treatment of tracing*)
   35.11  val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
   35.12 @@ -187,7 +187,7 @@
   35.13    | NONE => "");
   35.14  
   35.15  fun try_update_thy_only file =
   35.16 -  ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
   35.17 +  ThyLoad.cond_add_path (Path.dir (Path.explode file)) (fn () =>
   35.18      let val name = thy_name file in
   35.19        if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name))
   35.20        then update_thy_only name
   35.21 @@ -207,13 +207,13 @@
   35.22       (ThyInfo.touch_child_thys name;
   35.23        ThyInfo.pretend_use_thy_only name handle ERROR msg =>
   35.24         (warning msg; warning ("Failed to register theory: " ^ quote name);
   35.25 -        tell_file_retracted (Path.base (Path.unpack file))))
   35.26 +        tell_file_retracted (Path.base (Path.explode file))))
   35.27      else raise Toplevel.UNDEF
   35.28    end;
   35.29  
   35.30  fun vacuous_inform_file_processed file state =
   35.31   (warning ("No theory " ^ quote (thy_name file));
   35.32 -  tell_file_retracted (Path.base (Path.unpack file)));
   35.33 +  tell_file_retracted (Path.base (Path.explode file)));
   35.34  
   35.35  
   35.36  (* restart top-level loop (keeps most state information) *)
   35.37 @@ -371,7 +371,7 @@
   35.38  
   35.39  fun write_keywords s =
   35.40   (init_outer_syntax ();
   35.41 -  File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
   35.42 +  File.write (Path.explode ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
   35.43      (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
   35.44  
   35.45  end;
    36.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Dec 14 22:19:39 2006 +0100
    36.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Dec 15 00:08:06 2006 +0100
    36.3 @@ -271,7 +271,7 @@
    36.4  
    36.5  (* prepare theory context *)
    36.6  
    36.7 -val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
    36.8 +val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
    36.9  
   36.10  (* FIXME general treatment of tracing*)
   36.11  val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
   36.12 @@ -282,7 +282,7 @@
   36.13    | NONE => "");
   36.14  
   36.15  fun try_update_thy_only file =
   36.16 -  ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
   36.17 +  ThyLoad.cond_add_path (Path.dir (Path.explode file)) (fn () =>
   36.18      let val name = thy_name file in
   36.19        if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name))
   36.20        then update_thy_only name
   36.21 @@ -302,13 +302,13 @@
   36.22       (ThyInfo.touch_child_thys name;
   36.23        ThyInfo.pretend_use_thy_only name handle ERROR msg =>
   36.24         (warning msg; warning ("Failed to register theory: " ^ quote name);
   36.25 -        tell_file_retracted (Path.base (Path.unpack file))))
   36.26 +        tell_file_retracted (Path.base (Path.explode file))))
   36.27      else raise Toplevel.UNDEF
   36.28    end;
   36.29  
   36.30  fun vacuous_inform_file_processed file state =
   36.31   (warning ("No theory " ^ quote (thy_name file));
   36.32 -  tell_file_retracted (Path.base (Path.unpack file)));
   36.33 +  tell_file_retracted (Path.base (Path.explode file)));
   36.34  
   36.35  
   36.36  (* restart top-level loop (keeps most state information) *)
   36.37 @@ -387,15 +387,15 @@
   36.38  in
   36.39  fun send_pgip_config () =
   36.40      let
   36.41 -        val path = Path.unpack (config_file())
   36.42 +        val path = Path.explode (config_file())
   36.43          val exists = File.exists path
   36.44  
   36.45  	val wwwpage = 
   36.46 -	    (Url.unpack (isabelle_www()))
   36.47 +	    (Url.explode (isabelle_www()))
   36.48  	    handle _ => 
   36.49  		   (Output.panic 
   36.50  			("Error in URL in environment variable ISABELLE_HOMEPAGE.");
   36.51 -			Url.unpack isabellewww)
   36.52 +			Url.explode isabellewww)
   36.53  		     
   36.54  	val proverinfo =
   36.55              Proverinfo { name = "Isabelle",
   36.56 @@ -459,11 +459,11 @@
   36.57  
   36.58  fun use_thy_or_ml_file file =
   36.59      let
   36.60 -        val (path,extn) = Path.split_ext (Path.unpack file)
   36.61 +        val (path,extn) = Path.split_ext (Path.explode file)
   36.62      in
   36.63          case extn of
   36.64 -            "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
   36.65 -          | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
   36.66 +            "" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
   36.67 +          | "thy" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
   36.68            | "ML" => isarcmd ("use " ^ quote file)
   36.69            | other => error ("Don't know how to read a file with extension " ^ other)
   36.70      end
    37.1 --- a/src/Pure/ROOT.ML	Thu Dec 14 22:19:39 2006 +0100
    37.2 +++ b/src/Pure/ROOT.ML	Fri Dec 15 00:08:06 2006 +0100
    37.3 @@ -99,7 +99,7 @@
    37.4  (*final ML setup*)
    37.5  use "install_pp.ML";
    37.6  val use = ThyInfo.use;
    37.7 -val cd = File.cd o Path.unpack;
    37.8 +val cd = File.cd o Path.explode;
    37.9  ml_prompts "ML> " "ML# ";
   37.10  
   37.11  proofs := 0;
    38.1 --- a/src/Pure/Syntax/lexicon.ML	Thu Dec 14 22:19:39 2006 +0100
    38.2 +++ b/src/Pure/Syntax/lexicon.ML	Fri Dec 15 00:08:06 2006 +0100
    38.3 @@ -93,10 +93,10 @@
    38.4  
    38.5  (** basic scanners **)
    38.6  
    38.7 -val scan_letter_letdigs = Scan.one Symbol.is_letter -- Scan.any Symbol.is_letdig >> op ::;
    38.8 -val scan_digits1 = Scan.any1 Symbol.is_digit;
    38.9 -val scan_hex1 = Scan.any1 (Symbol.is_digit orf Symbol.is_hex_letter);
   38.10 -val scan_bin1 = Scan.any1 (fn s => s = "0" orelse s = "1");
   38.11 +val scan_letter_letdigs = Scan.one Symbol.is_letter -- Scan.many Symbol.is_letdig >> op ::;
   38.12 +val scan_digits1 = Scan.many1 Symbol.is_digit;
   38.13 +val scan_hex1 = Scan.many1 (Symbol.is_digit orf Symbol.is_hex_letter);
   38.14 +val scan_bin1 = Scan.many1 (fn s => s = "0" orelse s = "1");
   38.15  
   38.16  val scan_id = scan_letter_letdigs >> implode;
   38.17  val scan_longid = scan_id ^^ (Scan.repeat1 ($$ "." ^^ scan_id) >> implode);
   38.18 @@ -344,7 +344,7 @@
   38.19    let
   38.20      val scan =
   38.21        $$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol.is_eof) >> var ||
   38.22 -      Scan.any Symbol.not_eof >> (free o implode);
   38.23 +      Scan.many Symbol.not_eof >> (free o implode);
   38.24    in the (Scan.read Symbol.stopper scan (Symbol.explode str)) end;
   38.25  
   38.26  
   38.27 @@ -388,7 +388,7 @@
   38.28  val ten = ord "0" + 10;
   38.29  val a = ord "a";
   38.30  val A = ord "A";
   38.31 -val _ = assert (a > A) "Bad ASCII";
   38.32 +val _ = a > A orelse error "Bad ASCII";
   38.33  
   38.34  fun remap_hex c =
   38.35    let val x = ord c in
   38.36 @@ -421,8 +421,8 @@
   38.37  
   38.38  fun read_idents str =
   38.39    let
   38.40 -    val blanks = Scan.any Symbol.is_blank;
   38.41 -    val junk = Scan.any Symbol.not_eof;
   38.42 +    val blanks = Scan.many Symbol.is_blank;
   38.43 +    val junk = Scan.many Symbol.not_eof;
   38.44      val idents = Scan.repeat1 (blanks |-- scan_id --| blanks) -- junk;
   38.45    in
   38.46      (case Scan.read Symbol.stopper idents (Symbol.explode str) of
    39.1 --- a/src/Pure/Syntax/syn_ext.ML	Thu Dec 14 22:19:39 2006 +0100
    39.2 +++ b/src/Pure/Syntax/syn_ext.ML	Fri Dec 15 00:08:06 2006 +0100
    39.3 @@ -203,11 +203,11 @@
    39.4  val scan_sym =
    39.5    $$ "_" >> K (Argument ("", 0)) ||
    39.6    $$ "\\<index>" >> K index ||
    39.7 -  $$ "(" |-- Scan.any Symbol.is_digit >> (Bg o read_int) ||
    39.8 +  $$ "(" |-- Scan.many Symbol.is_digit >> (Bg o read_int) ||
    39.9    $$ ")" >> K En ||
   39.10    $$ "/" -- $$ "/" >> K (Brk ~1) ||
   39.11 -  $$ "/" |-- Scan.any Symbol.is_blank >> (Brk o length) ||
   39.12 -  Scan.any1 Symbol.is_blank >> (Space o implode) ||
   39.13 +  $$ "/" |-- Scan.many Symbol.is_blank >> (Brk o length) ||
   39.14 +  Scan.many1 Symbol.is_blank >> (Space o implode) ||
   39.15    Scan.repeat1 scan_delim_char >> (Delim o implode);
   39.16  
   39.17  val scan_symb =
    40.1 --- a/src/Pure/Thy/html.ML	Thu Dec 14 22:19:39 2006 +0100
    40.2 +++ b/src/Pure/Thy/html.ML	Fri Dec 15 00:08:06 2006 +0100
    40.3 @@ -266,13 +266,13 @@
    40.4  val keyword = enclose "<span class=\"keyword\">" "</span>" o output;
    40.5  val keyword_width = apfst (enclose "<span class=\"keyword\">" "</span>") o output_width;
    40.6  val file_name = enclose "<span class=\"filename\">" "</span>" o output;
    40.7 -val file_path = file_name o Url.pack;
    40.8 +val file_path = file_name o Url.implode;
    40.9  
   40.10  
   40.11  (* misc *)
   40.12  
   40.13  fun href_name s txt = "<a href=" ^ Library.quote s ^ ">" ^ txt ^ "</a>";
   40.14 -fun href_path path txt = href_name (Url.pack path) txt;
   40.15 +fun href_path path txt = href_name (Url.implode path) txt;
   40.16  
   40.17  fun href_opt_name NONE txt = txt
   40.18    | href_opt_name (SOME s) txt = href_name s txt;
   40.19 @@ -400,7 +400,7 @@
   40.20  (* ML file *)
   40.21  
   40.22  fun ml_file path str =
   40.23 -  begin_document ("File " ^ Url.pack path) ^
   40.24 +  begin_document ("File " ^ Url.implode path) ^
   40.25    "\n</div>\n<hr><div class=\"mlsource\">\n" ^
   40.26    verbatim str ^
   40.27    "\n</div>\n<hr>\n<div class=\"mlfooter\">\n" ^
    41.1 --- a/src/Pure/Thy/present.ML	Thu Dec 14 22:19:39 2006 +0100
    41.2 +++ b/src/Pure/Thy/present.ML	Fri Dec 15 00:08:06 2006 +0100
    41.3 @@ -60,15 +60,15 @@
    41.4  val graph_eps_path = Path.basic "session_graph.eps";
    41.5  
    41.6  val session_path = Path.basic ".session";
    41.7 -val session_entries_path = Path.unpack ".session/entries";
    41.8 -val pre_index_path = Path.unpack ".session/pre-index";
    41.9 +val session_entries_path = Path.explode ".session/entries";
   41.10 +val pre_index_path = Path.explode ".session/pre-index";
   41.11  
   41.12  fun mk_rel_path [] ys = Path.make ys
   41.13    | mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent)
   41.14    | mk_rel_path (ps as x :: xs) (qs as y :: ys) = if x = y then mk_rel_path xs ys else
   41.15        Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
   41.16  
   41.17 -fun show_path path = Path.pack (Path.append (File.pwd ()) path);
   41.18 +fun show_path path = Path.implode (Path.append (File.pwd ()) path);
   41.19  
   41.20  
   41.21  
   41.22 @@ -108,7 +108,7 @@
   41.23  fun display_graph gr =
   41.24    let
   41.25      val _ = writeln "Generating graph ...";
   41.26 -    val path = File.tmp_path (Path.unpack "tmp.graph");
   41.27 +    val path = File.tmp_path (Path.explode "tmp.graph");
   41.28      val _ = write_graph gr path;
   41.29      val _ = File.isatool ("browser -c " ^ File.shell_path path ^ " &");
   41.30    in () end;
   41.31 @@ -126,9 +126,9 @@
   41.32      path =
   41.33        if null session then "" else
   41.34        if is_some remote_path andalso not is_local then
   41.35 -        Url.pack (Url.append (the remote_path) (Url.File
   41.36 +        Url.implode (Url.append (the remote_path) (Url.File
   41.37            (Path.append (Path.make session) (html_path name))))
   41.38 -      else Path.pack (Path.append (mk_rel_path curr_sess session) (html_path name)),
   41.39 +      else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)),
   41.40      unfold = false,
   41.41      parents =
   41.42        map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) (ThyInfo.get_preds name)}
   41.43 @@ -271,7 +271,7 @@
   41.44  
   41.45  fun update_index dir name =
   41.46    (case try get_entries dir of
   41.47 -    NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.pack dir))
   41.48 +    NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.implode dir))
   41.49    | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir));
   41.50  
   41.51  
   41.52 @@ -323,7 +323,7 @@
   41.53          (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
   41.54          map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
   41.55        val index_text = HTML.begin_index (index_up_lnk, parent_name)
   41.56 -        (Url.File index_path, session_name) docs (Url.unpack "medium.html");
   41.57 +        (Url.File index_path, session_name) docs (Url.explode "medium.html");
   41.58      in
   41.59        session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
   41.60        info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
   41.61 @@ -407,10 +407,10 @@
   41.62        if length path > 1 then update_index parent_html_prefix name else ();
   41.63        (case readme of NONE => () | SOME path => File.copy path html_prefix);
   41.64        write_graph graph (Path.append html_prefix graph_path);
   41.65 -      File.copy (Path.unpack "~~/lib/browser/GraphBrowser.jar") html_prefix;
   41.66 +      File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
   41.67        List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
   41.68          (HTML.applet_pages name (Url.File index_path, name));
   41.69 -      File.copy (Path.unpack "~~/lib/html/isabelle.css") html_prefix;
   41.70 +      File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
   41.71        List.app finish_html thys;
   41.72        List.app (uncurry File.write) files;
   41.73        conditional verbose (fn () =>
   41.74 @@ -474,7 +474,7 @@
   41.75                HTML.ml_file (Url.File base) (File.read path));
   41.76              (SOME (Url.File base_html), Url.File raw_path, loadit)
   41.77            end
   41.78 -      | NONE => (warning ("Browser info: expected to find ML file" ^ quote (Path.pack raw_path));
   41.79 +      | NONE => (warning ("Browser info: expected to find ML file" ^ quote (Path.implode raw_path));
   41.80            (NONE, Url.File raw_path, loadit)));
   41.81  
   41.82      val files_html = map prep_file files;
   41.83 @@ -487,7 +487,7 @@
   41.84  
   41.85      val entry =
   41.86       {name = name, ID = ID_of path name, dir = sess_name, unfold = true,
   41.87 -      path = Path.pack (html_path name),
   41.88 +      path = Path.implode (html_path name),
   41.89        parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) raw_parents};
   41.90  
   41.91    in
   41.92 @@ -523,11 +523,11 @@
   41.93        let
   41.94          val base = Path.base path;
   41.95          val name =
   41.96 -          (case Path.pack (#1 (Path.split_ext base)) of "" => gensym "DUMMY" | s => s);
   41.97 +          (case Path.implode (#1 (Path.split_ext base)) of "" => gensym "DUMMY" | s => s);
   41.98        in
   41.99          if File.exists path then
  41.100            (Buffer.add (Latex.theory_entry name) tex_index, (name, base, File.read path))
  41.101 -        else error ("Bad file: " ^ quote (Path.pack path))
  41.102 +        else error ("Bad file: " ^ quote (Path.implode path))
  41.103        end;
  41.104      val (tex_index, srcs) = foldl_map prep_draft (Buffer.empty, src_paths);
  41.105  
  41.106 @@ -535,7 +535,7 @@
  41.107      val result_path = Path.append doc_path Path.parent;
  41.108      val _ = File.mkdir doc_path;
  41.109      val root_path = Path.append doc_path (Path.basic "root.tex");
  41.110 -    val _ = File.copy (Path.unpack "~~/lib/texinputs/draft.tex") root_path;
  41.111 +    val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path;
  41.112      val _ = File.isatool ("latex -o sty " ^ File.shell_path root_path);
  41.113      val _ = File.isatool ("latex -o syms " ^ File.shell_path root_path);
  41.114  
  41.115 @@ -547,7 +547,7 @@
  41.116  
  41.117      val _ = srcs |> List.app (fn (name, base, txt) =>
  41.118        Symbol.explode txt
  41.119 -      |> Latex.symbol_source (known_syms, known_ctrls) (Path.pack base)
  41.120 +      |> Latex.symbol_source (known_syms, known_ctrls) (Path.implode base)
  41.121        |> File.write (Path.append doc_path (tex_path name)));
  41.122      val _ = write_tex_index tex_index doc_path;
  41.123    in isatool_document false doc_format documentN "" doc_path result_path end;
    42.1 --- a/src/Pure/Thy/thm_database.ML	Thu Dec 14 22:19:39 2006 +0100
    42.2 +++ b/src/Pure/Thy/thm_database.ML	Fri Dec 15 00:08:06 2006 +0100
    42.3 @@ -78,7 +78,7 @@
    42.4                NameSpace.intern space xname = name then
    42.5              SOME (prfx, (bname, xname, length (the (Symtab.lookup thms name)) = 1))
    42.6            else NONE;
    42.7 -        val names = NameSpace.unpack name;
    42.8 +        val names = NameSpace.explode name;
    42.9        in
   42.10          (case #2 (chop (length names - 2) names) of
   42.11            [bname] => result "" bname
    43.1 --- a/src/Pure/Thy/thm_deps.ML	Thu Dec 14 22:19:39 2006 +0100
    43.2 +++ b/src/Pure/Thy/thm_deps.ML	Fri Dec 15 00:08:06 2006 +0100
    43.3 @@ -43,7 +43,7 @@
    43.4            if not (Symtab.defined gra name) then
    43.5              let
    43.6                val (gra', parents') = make_deps_graph prf' (gra, []);
    43.7 -              val prefx = #1 (Library.split_last (NameSpace.unpack name));
    43.8 +              val prefx = #1 (Library.split_last (NameSpace.explode name));
    43.9                val session =
   43.10                  (case prefx of
   43.11                    (x :: _) =>
    44.1 --- a/src/Pure/Thy/thy_info.ML	Thu Dec 14 22:19:39 2006 +0100
    44.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Dec 15 00:08:06 2006 +0100
    44.3 @@ -256,7 +256,7 @@
    44.4  fun provide path name info (deps as SOME {present, outdated, master, files}) =
    44.5       (if exists (equal path o #1) files then ()
    44.6        else warning (loader_msg "undeclared dependency of theory" [name] ^
    44.7 -        " on file: " ^ quote (Path.pack path));
    44.8 +        " on file: " ^ quote (Path.implode path));
    44.9        SOME (make_deps present outdated master (AList.update (op =) (path, SOME info) files)))
   44.10    | provide _ _ _ NONE = NONE;
   44.11  
   44.12 @@ -272,7 +272,7 @@
   44.13  
   44.14  fun load_file time path = Output.toplevel_errors (fn () =>
   44.15    if time then
   44.16 -    let val name = Path.pack path in
   44.17 +    let val name = Path.implode path in
   44.18        timeit (fn () =>
   44.19         (priority ("\n**** Starting file " ^ quote name ^ " ****");
   44.20          run_file path;
   44.21 @@ -280,8 +280,8 @@
   44.22      end
   44.23    else run_file path) ();
   44.24  
   44.25 -val use = load_file false o Path.unpack;
   44.26 -val time_use = load_file true o Path.unpack;
   44.27 +val use = load_file false o Path.explode;
   44.28 +val time_use = load_file true o Path.explode;
   44.29  
   44.30  end;
   44.31  
   44.32 @@ -303,7 +303,7 @@
   44.33        else #1 (ThyLoad.deps_thy dir name ml);
   44.34  
   44.35      val files = get_files name;
   44.36 -    val missing_files = map_filter (fn (path, NONE) => SOME (Path.pack path) | _ => NONE) files;
   44.37 +    val missing_files = map_filter (fn (path, NONE) => SOME (Path.implode path) | _ => NONE) files;
   44.38    in
   44.39      if null missing_files then ()
   44.40      else warning (loader_msg "unresolved dependencies of theory" [name] ^
   44.41 @@ -315,7 +315,7 @@
   44.42  
   44.43  (* require_thy *)
   44.44  
   44.45 -fun base_of_path s = Path.pack (Path.base (Path.unpack s));
   44.46 +fun base_of_path s = Path.implode (Path.base (Path.explode s));
   44.47  
   44.48  local
   44.49  
   44.50 @@ -333,7 +333,7 @@
   44.51    | SOME deps =>
   44.52        let
   44.53          fun get_name s = (case opt_path'' (lookup_deps s) of NONE => s
   44.54 -          | SOME p => Path.pack (Path.append p (Path.basic s)));
   44.55 +          | SOME p => Path.implode (Path.append p (Path.basic s)));
   44.56          val same_deps = (NONE, map get_name (thy_graph Graph.imm_preds name))
   44.57        in
   44.58          (case deps of
   44.59 @@ -349,8 +349,8 @@
   44.60  
   44.61  fun require_thy really ml time strict keep_strict initiators prfx (visited, str) =
   44.62    let
   44.63 -    val path = Path.expand (Path.unpack str);
   44.64 -    val name = Path.pack (Path.base path);
   44.65 +    val path = Path.expand (Path.explode str);
   44.66 +    val name = Path.implode (Path.base path);
   44.67    in
   44.68      if member (op =) initiators name then error (cycle_msg initiators) else ();
   44.69      if known_thy name andalso is_finished name orelse member (op =) visited name then
   44.70 @@ -422,7 +422,7 @@
   44.71    let val illegal = map (fn ext => Path.ext ext (Path.basic name)) ThyLoad.ml_exts in
   44.72      (case find_first (member (op =) illegal o Path.base o Path.expand o #1) uses of
   44.73        NONE => ()
   44.74 -    | SOME (path, _) => error ("Illegal use of theory ML file: " ^ quote (Path.pack path)))
   44.75 +    | SOME (path, _) => error ("Illegal use of theory ML file: " ^ quote (Path.implode path)))
   44.76    end;
   44.77  
   44.78  fun begin_theory present name parents uses int =
    45.1 --- a/src/Pure/Thy/thy_load.ML	Thu Dec 14 22:19:39 2006 +0100
    45.2 +++ b/src/Pure/Thy/thy_load.ML	Fri Dec 15 00:08:06 2006 +0100
    45.3 @@ -49,12 +49,12 @@
    45.4  val load_path = ref [Path.current];
    45.5  fun change_path f = load_path := f (! load_path);
    45.6  
    45.7 -fun show_path () = map Path.pack (! load_path);
    45.8 -fun del_path s = change_path (filter_out (equal (Path.unpack s)));
    45.9 -fun add_path s = (del_path s; change_path (cons (Path.unpack s)));
   45.10 -fun path_add s = (del_path s; change_path (fn path => path @ [Path.unpack s]));
   45.11 +fun show_path () = map Path.implode (! load_path);
   45.12 +fun del_path s = change_path (filter_out (equal (Path.explode s)));
   45.13 +fun add_path s = (del_path s; change_path (cons (Path.explode s)));
   45.14 +fun path_add s = (del_path s; change_path (fn path => path @ [Path.explode s]));
   45.15  fun reset_path () = load_path := [Path.current];
   45.16 -fun with_paths ss f x = Library.setmp load_path (! load_path @ map Path.unpack ss) f x;
   45.17 +fun with_paths ss f x = Library.setmp load_path (! load_path @ map Path.explode ss) f x;
   45.18  fun with_path s f x = with_paths [s] f x;
   45.19  
   45.20  fun cond_add_path path f x =
   45.21 @@ -95,7 +95,7 @@
   45.22  
   45.23  fun load_file current raw_path =
   45.24    (case check_file current raw_path of
   45.25 -    NONE => error ("Could not find ML file " ^ quote (Path.pack raw_path))
   45.26 +    NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))
   45.27    | SOME (path, info) => (File.use path; (path, info)));
   45.28  
   45.29  
   45.30 @@ -113,7 +113,7 @@
   45.31  fun check_thy_aux (name, ml) =
   45.32    let val thy_file = thy_path name in
   45.33      case check_file NONE thy_file of
   45.34 -      NONE => error ("Could not find theory file " ^ quote (Path.pack thy_file) ^
   45.35 +      NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^
   45.36          " in dir(s) " ^ commas_quote (show_path ()))
   45.37      | SOME thy_info => (thy_info, if ml then check_file NONE (ml_path name) else NONE)
   45.38    end;
    46.1 --- a/src/Pure/Tools/codegen_names.ML	Thu Dec 14 22:19:39 2006 +0100
    46.2 +++ b/src/Pure/Tools/codegen_names.ML	Fri Dec 15 00:08:06 2006 +0100
    46.3 @@ -176,12 +176,12 @@
    46.4    let
    46.5      fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
    46.6      val is_junk = not o is_valid andf Symbol.not_eof;
    46.7 -    val junk = Scan.any is_junk;
    46.8 +    val junk = Scan.many is_junk;
    46.9      val scan_valids = Symbol.scanner "Malformed input"
   46.10        ((junk |--
   46.11 -        (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.any is_valid >> implode)
   46.12 +        (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
   46.13          --| junk))
   46.14 -      -- Scan.repeat ((Scan.any1 is_valid >> implode) --| junk) >> op ::);
   46.15 +      -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::);
   46.16    in explode #> scan_valids #> space_implode "_" end;
   46.17  
   46.18  fun purify_op "0" = "zero"
   46.19 @@ -212,11 +212,11 @@
   46.20  
   46.21  fun check_modulename mn =
   46.22    let
   46.23 -    val mns = NameSpace.unpack mn;
   46.24 +    val mns = NameSpace.explode mn;
   46.25      val mns' = map purify_upper mns;
   46.26    in
   46.27      if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
   46.28 -      ^ "perhaps try " ^ quote (NameSpace.pack mns'))
   46.29 +      ^ "perhaps try " ^ quote (NameSpace.implode mns'))
   46.30    end
   46.31  
   46.32  fun purify_var "" = "x"
   46.33 @@ -234,9 +234,9 @@
   46.34  
   46.35  fun policy thy get_basename get_thyname name =
   46.36    let
   46.37 -    val prefix = (purify_prefix o NameSpace.unpack o get_thyname thy) name;
   46.38 +    val prefix = (purify_prefix o NameSpace.explode o get_thyname thy) name;
   46.39      val base = (purify_base o get_basename) name;
   46.40 -  in NameSpace.pack (prefix @ [base]) end;
   46.41 +  in NameSpace.implode (prefix @ [base]) end;
   46.42  
   46.43  fun class_policy thy = policy thy NameSpace.base thyname_of_class;
   46.44  fun tyco_policy thy = policy thy NameSpace.base thyname_of_tyco;
   46.45 @@ -258,10 +258,10 @@
   46.46    case force_thyname thy (c, tys)
   46.47     of NONE => policy thy NameSpace.base thyname_of_const c
   46.48      | SOME thyname => let
   46.49 -        val prefix = (purify_prefix o NameSpace.unpack) thyname;
   46.50 +        val prefix = (purify_prefix o NameSpace.explode) thyname;
   46.51          val tycos = map_filter (fn Type (tyco, _) => SOME tyco | _ => NONE) tys;
   46.52          val base = map (purify_base o NameSpace.base) (c :: tycos);
   46.53 -      in NameSpace.pack (prefix @ [space_implode "_" base]) end;
   46.54 +      in NameSpace.implode (prefix @ [space_implode "_" base]) end;
   46.55  
   46.56  
   46.57  (* shallow name spaces *)
   46.58 @@ -274,20 +274,20 @@
   46.59  
   46.60  fun add_nsp shallow name =
   46.61    name
   46.62 -  |> NameSpace.unpack
   46.63 +  |> NameSpace.explode
   46.64    |> split_last
   46.65    |> apsnd (single #> cons shallow)
   46.66    |> (op @)
   46.67 -  |> NameSpace.pack;
   46.68 +  |> NameSpace.implode;
   46.69  
   46.70  fun dest_nsp nsp nspname =
   46.71    let
   46.72 -    val xs = NameSpace.unpack nspname;
   46.73 +    val xs = NameSpace.explode nspname;
   46.74      val (ys, base) = split_last xs;
   46.75      val (module, shallow) = split_last ys;
   46.76    in
   46.77      if nsp = shallow
   46.78 -   then (SOME o NameSpace.pack) (module @ [base])
   46.79 +   then (SOME o NameSpace.implode) (module @ [base])
   46.80      else NONE
   46.81    end;
   46.82  
    47.1 --- a/src/Pure/Tools/codegen_serializer.ML	Thu Dec 14 22:19:39 2006 +0100
    47.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Fri Dec 15 00:08:06 2006 +0100
    47.3 @@ -235,7 +235,7 @@
    47.4  
    47.5  fun dest_name name =
    47.6    let
    47.7 -    val (names, name_base) = (split_last o NameSpace.unpack) name;
    47.8 +    val (names, name_base) = (split_last o NameSpace.explode) name;
    47.9      val (names_mod, name_shallow) = split_last names;
   47.10    in (names_mod, (name_shallow, name_base)) end;
   47.11  
   47.12 @@ -257,7 +257,7 @@
   47.13      fun dictvar v = 
   47.14        first_upper v ^ "_";
   47.15      val label = translate_string (fn "." => "__" | c => c)
   47.16 -      o NameSpace.pack o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.unpack;
   47.17 +      o NameSpace.implode o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.explode;
   47.18      fun pr_tyvar (v, []) =
   47.19            str "()"
   47.20        | pr_tyvar (v, sort) =
   47.21 @@ -584,7 +584,7 @@
   47.22      fun dictvar v = 
   47.23        first_upper v ^ "_";
   47.24      val label = translate_string (fn "." => "__" | c => c)
   47.25 -      o NameSpace.pack o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.unpack;
   47.26 +      o NameSpace.implode o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.explode;
   47.27      fun pr_tyvar (v, []) =
   47.28            str "()"
   47.29        | pr_tyvar (v, sort) =
   47.30 @@ -924,9 +924,9 @@
   47.31      val init_vars = CodegenThingol.make_vars (ML_Syntax.reserved_names @ reserved_user);
   47.32      fun name_modl modl =
   47.33        let
   47.34 -        val modlname = NameSpace.pack modl
   47.35 +        val modlname = NameSpace.implode modl
   47.36        in case module_alias modlname
   47.37 -       of SOME modlname' => NameSpace.unpack modlname'
   47.38 +       of SOME modlname' => NameSpace.explode modlname'
   47.39          | NONE => map (fn name => (the_single o fst)
   47.40              (Name.variants [name] empty_names)) modl
   47.41        end;
   47.42 @@ -992,14 +992,14 @@
   47.43              val (modl'', defname'') = (apfst name_modl o dest_name) name'';
   47.44            in if modl' = modl'' then
   47.45              map_node modl'
   47.46 -              (Graph.add_edge (NameSpace.pack (modl @ [fst defname, snd defname]), name''))
   47.47 +              (Graph.add_edge (NameSpace.implode (modl @ [fst defname, snd defname]), name''))
   47.48            else let
   47.49              val (common, (diff1::_, diff2::_)) = chop_prefix (op =) (modl', modl'');
   47.50            in
   47.51              map_node common
   47.52                (fn gr => Graph.add_edge_acyclic (diff1, diff2) gr
   47.53                  handle Graph.CYCLES _ => error ("Dependency "
   47.54 -                  ^ quote (NameSpace.pack (modl' @ [fst defname, snd defname]))
   47.55 +                  ^ quote (NameSpace.implode (modl' @ [fst defname, snd defname]))
   47.56                    ^ " -> " ^ quote name'' ^ " would result in module dependency cycle"))
   47.57            end end;
   47.58        in
   47.59 @@ -1039,7 +1039,7 @@
   47.60            |> fold (fn m => fn g => case Graph.get_node g m
   47.61                of Module (_, (_, g)) => g) modl'
   47.62            |> (fn g => case Graph.get_node g name of Def (defname, _) => defname);
   47.63 -      in NameSpace.pack (remainder @ [defname']) end handle Graph.UNDEF _ =>
   47.64 +      in NameSpace.implode (remainder @ [defname']) end handle Graph.UNDEF _ =>
   47.65          "(raise Fail \"undefined name " ^ name ^ "\")";
   47.66      fun the_prolog modlname = case module_prolog modlname
   47.67       of NONE => []
   47.68 @@ -1049,7 +1049,7 @@
   47.69        | pr_node prefix (Def (_, SOME def)) =
   47.70            SOME (pr_def tyco_syntax const_syntax init_vars (deresolver prefix) def)
   47.71        | pr_node prefix (Module (dmodlname, (_, nodes))) =
   47.72 -          SOME (pr_modl dmodlname (the_prolog (NameSpace.pack (prefix @ [dmodlname]))
   47.73 +          SOME (pr_modl dmodlname (the_prolog (NameSpace.implode (prefix @ [dmodlname]))
   47.74              @ separate (str "") ((map_filter (pr_node (prefix @ [dmodlname]) o Graph.get_node nodes)
   47.75                  o rev o flat o Graph.strong_conn) nodes)));
   47.76      val p = pr_modl "ROOT" (the_prolog "" @ separate (str "") ((map_filter
   47.77 @@ -1058,7 +1058,7 @@
   47.78  
   47.79  val isar_seri_sml =
   47.80    let
   47.81 -    fun output_file file p = File.write (Path.unpack file) (Pretty.output p ^ "\n");
   47.82 +    fun output_file file p = File.write (Path.explode file) (Pretty.output p ^ "\n");
   47.83      fun output_diag p = Pretty.writeln p;
   47.84      fun output_internal p = use_text Output.ml_output false (Pretty.output p);
   47.85    in
   47.86 @@ -1070,7 +1070,7 @@
   47.87  
   47.88  val isar_seri_ocaml =
   47.89    let
   47.90 -    fun output_file file p = File.write (Path.unpack file) (Pretty.output p ^ "\n");
   47.91 +    fun output_file file p = File.write (Path.explode file) (Pretty.output p ^ "\n");
   47.92      fun output_diag p = Pretty.writeln p;
   47.93    in
   47.94      parse_args ((Args.$$$ "-" >> K output_diag
   47.95 @@ -1330,16 +1330,16 @@
   47.96  fun seri_haskell module_prefix destination string_classes reserved_user module_alias module_prolog
   47.97    class_syntax tyco_syntax const_syntax code =
   47.98    let
   47.99 -    val _ = Option.map File.assert destination;
  47.100 +    val _ = Option.map File.check destination;
  47.101      val empty_names = Name.make_context (reserved_haskell @ reserved_user);
  47.102      fun name_modl modl =
  47.103        let
  47.104 -        val modlname = NameSpace.pack modl
  47.105 +        val modlname = NameSpace.implode modl
  47.106        in (modlname, case module_alias modlname
  47.107         of SOME modlname' => (case module_prefix
  47.108              of NONE => modlname'
  47.109               | SOME module_prefix => NameSpace.append module_prefix modlname')
  47.110 -        | NONE => NameSpace.pack (map_filter I (module_prefix :: map (fn name => (SOME o the_single o fst)
  47.111 +        | NONE => NameSpace.implode (map_filter I (module_prefix :: map (fn name => (SOME o the_single o fst)
  47.112              (Name.variants [name] empty_names)) modl)))
  47.113        end;
  47.114      fun add_def (name, (def, deps)) =
  47.115 @@ -1409,8 +1409,8 @@
  47.116      fun write_module (SOME destination) modlname p =
  47.117            let
  47.118              val filename = case modlname
  47.119 -             of "" => Path.unpack "Main.hs"
  47.120 -              | _ => (Path.ext "hs" o Path.unpack o implode o separate "/" o NameSpace.unpack) modlname;
  47.121 +             of "" => Path.explode "Main.hs"
  47.122 +              | _ => (Path.ext "hs" o Path.explode o implode o separate "/" o NameSpace.explode) modlname;
  47.123              val pathname = Path.append destination filename;
  47.124              val _ = File.mkdir (Path.dir pathname);
  47.125            in File.write pathname (Pretty.setmp_margin 999999 Pretty.output p ^ "\n") end
  47.126 @@ -1435,7 +1435,7 @@
  47.127      -- Scan.optional (Args.$$$ "string_classes" >> K true) false
  47.128      -- (Args.$$$ "-" >> K NONE || Args.name >> SOME)
  47.129      >> (fn ((module_prefix, string_classes), destination) =>
  47.130 -      seri_haskell module_prefix (Option.map Path.unpack destination) string_classes));
  47.131 +      seri_haskell module_prefix (Option.map Path.explode destination) string_classes));
  47.132  
  47.133  
  47.134  (** diagnosis serializer **)
    48.1 --- a/src/Pure/codegen.ML	Thu Dec 14 22:19:39 2006 +0100
    48.2 +++ b/src/Pure/codegen.ML	Fri Dec 15 00:08:06 2006 +0100
    48.3 @@ -443,7 +443,7 @@
    48.4              | (true, "isup") => "" :: check_str zs
    48.5              | (ctrl, s') => (if ctrl then "ctrl_" ^ s' else s') :: check_str zs)
    48.6          | (ys, zs) => implode ys :: check_str zs);
    48.7 -    val s' = space_implode "_" (maps (check_str o Symbol.explode) (NameSpace.unpack s))
    48.8 +    val s' = space_implode "_" (maps (check_str o Symbol.explode) (NameSpace.explode s))
    48.9    in
   48.10      if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s'
   48.11    end;
   48.12 @@ -453,7 +453,7 @@
   48.13      fun find_name [] = sys_error "mk_long_id"
   48.14        | find_name (ys :: yss) =
   48.15            let
   48.16 -            val s' = NameSpace.pack ys
   48.17 +            val s' = NameSpace.implode ys
   48.18              val s'' = NameSpace.append module s'
   48.19            in case Symtab.lookup used s'' of
   48.20                NONE => ((module, s'),
   48.21 @@ -462,7 +462,7 @@
   48.22              | SOME _ => find_name yss
   48.23            end
   48.24    in case Symtab.lookup tab s of
   48.25 -      NONE => find_name (Library.suffixes1 (NameSpace.unpack s))
   48.26 +      NONE => find_name (Library.suffixes1 (NameSpace.explode s))
   48.27      | SOME name => (name, p)
   48.28    end;
   48.29  
   48.30 @@ -874,9 +874,9 @@
   48.31  fun gen_generate_code prep_term thy modules module =
   48.32    setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs =>
   48.33    let
   48.34 -    val _ = assert (module <> "" orelse
   48.35 +    val _ = (module <> "" orelse
   48.36          member (op =) (!mode) "library" andalso forall (equal "" o fst) xs)
   48.37 -      "missing module name";
   48.38 +      orelse error "missing module name";
   48.39      val graphs = get_modules thy;
   48.40      val defs = mk_deftab thy;
   48.41      val gr = new_node ("<Top>", (NONE, module, ""))
   48.42 @@ -958,10 +958,10 @@
   48.43  
   48.44  fun test_term thy sz i t =
   48.45    let
   48.46 -    val _ = assert (null (term_tvars t) andalso null (term_tfrees t))
   48.47 -      "Term to be tested contains type variables";
   48.48 -    val _ = assert (null (term_vars t))
   48.49 -      "Term to be tested contains schematic variables";
   48.50 +    val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
   48.51 +      error "Term to be tested contains type variables";
   48.52 +    val _ = null (term_vars t) orelse
   48.53 +      error "Term to be tested contains schematic variables";
   48.54      val frees = map dest_Free (term_frees t);
   48.55      val frees' = frees ~~
   48.56        map (fn i => "arg" ^ string_of_int i) (1 upto length frees);
   48.57 @@ -1028,10 +1028,10 @@
   48.58  
   48.59  fun eval_term thy = setmp print_mode [] (fn t =>
   48.60    let
   48.61 -    val _ = assert (null (term_tvars t) andalso null (term_tfrees t))
   48.62 -      "Term to be evaluated contains type variables";
   48.63 -    val _ = assert (null (term_vars t) andalso null (term_frees t))
   48.64 -      "Term to be evaluated contains variables";
   48.65 +    val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
   48.66 +      error "Term to be evaluated contains type variables";
   48.67 +    val _ = (null (term_vars t) andalso null (term_frees t)) orelse
   48.68 +      error "Term to be evaluated contains variables";
   48.69      val (code, gr) = setmp mode ["term_of"]
   48.70        (generate_code_i thy [] "Generated") [("result", t)];
   48.71      val s = "structure EvalTerm =\nstruct\n\n" ^
   48.72 @@ -1155,10 +1155,10 @@
   48.73         | SOME fname =>
   48.74             if lib then
   48.75               app (fn (name, s) => File.write
   48.76 -                 (Path.append (Path.unpack fname) (Path.basic (name ^ ".ML"))) s)
   48.77 +                 (Path.append (Path.explode fname) (Path.basic (name ^ ".ML"))) s)
   48.78                 (("ROOT", implode (map (fn (name, _) =>
   48.79                     "use \"" ^ name ^ ".ML\";\n") code)) :: code)
   48.80 -           else File.write (Path.unpack fname) (snd (hd code)));
   48.81 +           else File.write (Path.explode fname) (snd (hd code)));
   48.82             if lib then thy
   48.83             else map_modules (Symtab.update (module, gr)) thy)
   48.84       end));
    49.1 --- a/src/Pure/proof_general.ML	Thu Dec 14 22:19:39 2006 +0100
    49.2 +++ b/src/Pure/proof_general.ML	Fri Dec 15 00:08:06 2006 +0100
    49.3 @@ -402,7 +402,7 @@
    49.4  
    49.5  (* prepare theory context *)
    49.6  
    49.7 -val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
    49.8 +val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
    49.9  
   49.10  (* FIXME general treatment of tracing*)
   49.11  val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
   49.12 @@ -413,7 +413,7 @@
   49.13    | NONE => "");
   49.14  
   49.15  fun try_update_thy_only file =
   49.16 -  ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
   49.17 +  ThyLoad.cond_add_path (Path.dir (Path.explode file)) (fn () =>
   49.18      let val name = thy_name file in
   49.19        if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name))
   49.20        then update_thy_only name
   49.21 @@ -433,13 +433,13 @@
   49.22       (ThyInfo.touch_child_thys name;
   49.23        ThyInfo.pretend_use_thy_only name handle ERROR msg =>
   49.24         (warning msg; warning ("Failed to register theory: " ^ quote name);
   49.25 -        tell_file_retracted (Path.base (Path.unpack file))))
   49.26 +        tell_file_retracted (Path.base (Path.explode file))))
   49.27      else raise Toplevel.UNDEF
   49.28    end;
   49.29  
   49.30  fun vacuous_inform_file_processed file state =
   49.31   (warning ("No theory " ^ quote (thy_name file));
   49.32 -  tell_file_retracted (Path.base (Path.unpack file)));
   49.33 +  tell_file_retracted (Path.base (Path.explode file)));
   49.34  
   49.35  
   49.36  (* restart top-level loop (keeps most state information) *)
   49.37 @@ -653,7 +653,7 @@
   49.38  in
   49.39  fun send_pgip_config () =
   49.40      let
   49.41 -        val path = Path.unpack (config_file())
   49.42 +        val path = Path.explode (config_file())
   49.43          val exists = File.exists path
   49.44          val proverinfo =
   49.45              XML.element "proverinfo"
   49.46 @@ -678,7 +678,7 @@
   49.47  fun send_informguise (openfile, opentheory, openproofpos) =
   49.48      let val guisefile =
   49.49              case openfile of SOME f => [XML.element "guisefile"
   49.50 -                                                    [("url",Url.pack (Url.File (Path.unpack f)))] []]
   49.51 +                                                    [("url",Url.implode (Url.File (Path.explode f)))] []]
   49.52                             | _ => []
   49.53          val guisetheory =
   49.54              case opentheory of SOME t => [XML.element "guisetheory" [("thyname", t)] []]
   49.55 @@ -1172,11 +1172,11 @@
   49.56  
   49.57  fun use_thy_or_ml_file file =
   49.58      let
   49.59 -        val (path,extn) = Path.split_ext (Path.unpack file)
   49.60 +        val (path,extn) = Path.split_ext (Path.explode file)
   49.61      in
   49.62          case extn of
   49.63 -            "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
   49.64 -          | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
   49.65 +            "" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
   49.66 +          | "thy" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
   49.67            | "ML" => isarcmd ("use " ^ quote file)
   49.68            | other => error ("Don't know how to read a file with extension " ^ other)
   49.69      end
   49.70 @@ -1199,7 +1199,7 @@
   49.71    val name_attr = xmlattr "name"
   49.72  
   49.73    fun localfile_of_url url = (* only handle file:/// or file://localhost/ *)
   49.74 -      case Url.unpack url of
   49.75 +      case Url.explode url of
   49.76            (Url.File path) => File.platform_path path
   49.77          | _ => error ("Cannot access non-local URL " ^ url)
   49.78  
   49.79 @@ -1515,7 +1515,7 @@
   49.80  
   49.81  fun write_keywords s =
   49.82   (init_outer_syntax ();
   49.83 -  File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
   49.84 +  File.write (Path.explode ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
   49.85      (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
   49.86  
   49.87  end;
    50.1 --- a/src/Pure/type.ML	Thu Dec 14 22:19:39 2006 +0100
    50.2 +++ b/src/Pure/type.ML	Fri Dec 15 00:08:06 2006 +0100
    50.3 @@ -535,7 +535,8 @@
    50.4  fun map_types f = map_tsig (fn (classes, default, types) =>
    50.5    let
    50.6      val (space', tab') = f types;
    50.7 -    val _ = assert (NameSpace.intern space' "dummy" = "dummy") "Illegal declaration of dummy type";
    50.8 +    val _ = NameSpace.intern space' "dummy" = "dummy" orelse
    50.9 +      error "Illegal declaration of dummy type";
   50.10    in (classes, default, (space', tab')) end);
   50.11  
   50.12  fun syntactic types (Type (c, Ts)) =