# HG changeset patch
# User wenzelm
# Date 1166137686 -3600
# Node ID 05f57309170c43b63e229717582686ea82672fe5
# Parent  f9d085c2625c0b3bac7c53f24040105bf95f42a4
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;

diff -r f9d085c2625c -r 05f57309170c TFL/casesplit.ML
--- a/TFL/casesplit.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/TFL/casesplit.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -268,7 +268,7 @@
 having to (re)search for variables to split. *)
 fun splitto splitths genth =
     let
-      val _ = assert (not (null splitths)) "splitto: no given splitths";
+      val _ = not (null splitths) orelse error "splitto: no given splitths";
       val sgn = Thm.sign_of_thm genth;
 
       (* check if we are a member of splitths - FIXME: quicker and
diff -r f9d085c2625c -r 05f57309170c TFL/rules.ML
--- a/TFL/rules.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/TFL/rules.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -698,9 +698,8 @@
                   end
              fun pq_eliminate (thm,sign,vlist,imp_body,lhs_eq) =
               let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
-                  val dummy = assert (forall (op aconv)
-                                      (ListPair.zip (vlist, args)))
-                               "assertion failed in CONTEXT_REWRITE_RULE"
+                  val dummy = forall (op aconv) (ListPair.zip (vlist, args))
+                    orelse error "assertion failed in CONTEXT_REWRITE_RULE"
                   val imp_body1 = subst_free (ListPair.zip (args, vstrl))
                                              imp_body
                   val tych = cterm_of sign
diff -r f9d085c2625c -r 05f57309170c src/HOL/Import/hol4rews.ML
--- a/src/HOL/Import/hol4rews.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Import/hol4rews.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -584,7 +584,7 @@
 	    if internal
 	    then
 		let
-		    val paths = NameSpace.unpack isa
+		    val paths = NameSpace.explode isa
 		    val i = Library.drop(length paths - 2,paths)
 		in
 		    case i of
@@ -638,10 +638,10 @@
 
 	fun gen2replay in_thy out_thy s = 
 	    let
-		val ss = NameSpace.unpack s
+		val ss = NameSpace.explode s
 	    in
 		if (hd ss = in_thy) then 
-		    NameSpace.pack (out_thy::(tl ss))
+		    NameSpace.implode (out_thy::(tl ss))
 		else
 		    s
 	    end 
diff -r f9d085c2625c -r 05f57309170c src/HOL/Import/importrecorder.ML
--- a/src/HOL/Import/importrecorder.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Import/importrecorder.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -188,7 +188,7 @@
 fun set_skip_import_dir dir = (history_dir := dir)
 fun get_skip_import_dir () = !history_dir
 
-fun get_filename thyname = Path.pack (Path.append (Path.unpack (the (get_skip_import_dir ()))) (Path.unpack (thyname^".history")))
+fun get_filename thyname = Path.implode (Path.append (Path.explode (the (get_skip_import_dir ()))) (Path.explode (thyname^".history")))
 
 fun save_history thyname = 
     if get_skip_import () then
@@ -202,7 +202,7 @@
 	    val filename = get_filename thyname
 	    val _ = writeln "load_history / before"
 	    val _ = 
-		if File.exists (Path.unpack filename) then					
+		if File.exists (Path.explode filename) then					
 		    (history := XMLConv.read_from_file history_of_xml (get_filename thyname)) 
 		else
 		    clear_history ()
diff -r f9d085c2625c -r 05f57309170c src/HOL/Import/xmlconv.ML
--- a/src/HOL/Import/xmlconv.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Import/xmlconv.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -243,12 +243,12 @@
     ) e
 
 
-fun to_file f output fname x = File.write (Path.unpack fname) (f (output x))
+fun to_file f output fname x = File.write (Path.explode fname) (f (output x))
  
 fun from_file f input fname = 
     let
 	val _ = writeln "read_from_file enter"
-	val s = File.read (Path.unpack fname)
+	val s = File.read (Path.explode fname)
 	val _ = writeln "done: read file"
 	val tree = timeit (fn () => f s)
 	val _ = writeln "done: tree"
diff -r f9d085c2625c -r 05f57309170c src/HOL/Matrix/cplex/Cplex_tools.ML
--- a/src/HOL/Matrix/cplex/Cplex_tools.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Matrix/cplex/Cplex_tools.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -1136,7 +1136,7 @@
 
 exception Execute of string;
 
-fun tmp_file s = Path.pack (Path.expand (File.tmp_path (Path.make [s])));
+fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s])));
 fun wrap s = "\""^s^"\"";
 
 fun solve_glpk prog =
diff -r f9d085c2625c -r 05f57309170c src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -733,8 +733,8 @@
 
     (** strips the "_Rep" in type names *)
     fun strip_nth_name i s =
-      let val xs = NameSpace.unpack s;
-      in NameSpace.pack (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
+      let val xs = NameSpace.explode s;
+      in NameSpace.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
 
     val (descr'', ndescr) = ListPair.unzip (List.mapPartial
       (fn (i, ("Nominal.noption", _, _)) => NONE
diff -r f9d085c2625c -r 05f57309170c src/HOL/Tools/ATP/AtpCommunication.ML
--- a/src/HOL/Tools/ATP/AtpCommunication.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/ATP/AtpCommunication.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -128,7 +128,8 @@
 (*Return everything in s that comes before the string t*)
 fun cut_before t s = 
   let val (s1,s2) = Substring.position t (Substring.full s)
-      val _ = assert (Substring.size s2 <> 0) "cut_before: string not found" 
+      val _ = Substring.size s2 <> 0
+        orelse error "cut_before: string not found"
   in Substring.string s2 end;
 
 val start_E = "# Proof object starts here."
diff -r f9d085c2625c -r 05f57309170c src/HOL/Tools/function_package/fundef_lib.ML
--- a/src/HOL/Tools/function_package/fundef_lib.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -54,7 +54,8 @@
       val (_, ctx') = ProofContext.add_fixes_i [(n', SOME T, NoSyn)] ctx
 
       val (n'', body) = Term.dest_abs (n', T, b) 
-      val _ = assert (n' = n'') "dest_all_ctx" (* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *)
+      val _ = (n' = n'') orelse error "dest_all_ctx"
+      (* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *)
 
       val (ctx'', vs, bd) = dest_all_all_ctx ctx' body
     in
@@ -133,4 +134,4 @@
 
 
 
-end
\ No newline at end of file
+end
diff -r f9d085c2625c -r 05f57309170c src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -296,12 +296,12 @@
     val (_, params) = strip_comb S;
     val params' = map dest_Var params;
     val rss = [] |> fold add_rule intrs;
-    val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss)));
+    val (prfx, _) = split_last (NameSpace.explode (fst (hd rss)));
     val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
 
     val thy1 = thy |>
       Theory.root_path |>
-      Theory.add_path (NameSpace.pack prfx);
+      Theory.add_path (NameSpace.implode prfx);
     val (ty_eqs, rlz_eqs) = split_list
       (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs rs) rss);
 
diff -r f9d085c2625c -r 05f57309170c src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/record_package.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -439,8 +439,8 @@
 fun get_extT_fields thy T =
   let
     val ((name,Ts),moreT) = dest_recT T;
-    val recname = let val (nm::recn::rst) = rev (NameSpace.unpack name)
-                  in NameSpace.pack (rev (nm::rst)) end;
+    val recname = let val (nm::recn::rst) = rev (NameSpace.explode name)
+                  in NameSpace.implode (rev (nm::rst)) end;
     val midx = maxidx_of_typs (moreT::Ts);
     val varifyT = varifyT midx;
     val {records,extfields,...} = RecordsData.get thy;
diff -r f9d085c2625c -r 05f57309170c src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/res_atp.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -99,13 +99,13 @@
       "" => error  ("Isabelle environment variable " ^ evar ^ " not defined")
     | home =>
         let val path = home ^ "/" ^ base
-        in  if File.exists (File.unpack_platform_path path) then path
+        in  if File.exists (File.explode_platform_path path) then path
             else error ("Could not find the file " ^ path)
         end;
 
 fun probfile_nosuffix _ =
   if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
-  else if File.exists (File.unpack_platform_path (!destdir))
+  else if File.exists (File.explode_platform_path (!destdir))
   then !destdir ^ "/" ^ !problem_name
   else error ("No such directory: " ^ !destdir);
 
@@ -149,7 +149,7 @@
     let val file = !problem_name
     in
         if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
-        else if File.exists (File.unpack_platform_path (!destdir))
+        else if File.exists (File.explode_platform_path (!destdir))
         then !destdir ^ "/" ^ file
         else error ("No such directory: " ^ !destdir)
     end;
@@ -463,7 +463,7 @@
 (*Reject theorems with names like "List.filter.filter_list_def" or
   "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
 fun is_package_def a =
-  let val names = NameSpace.unpack a
+  let val names = NameSpace.explode a
   in
      length names > 2 andalso
      not (hd names = "local") andalso
@@ -820,7 +820,7 @@
   end
 
 fun trace_array fname =
-  let val path = File.unpack_platform_path fname
+  let val path = File.explode_platform_path fname
   in  Array.app (File.append path o (fn s => s ^ "\n"))  end;
 
 (*Converting a subgoal into negated conjecture clauses*)
diff -r f9d085c2625c -r 05f57309170c src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -460,7 +460,7 @@
   handle THM _ => [];
 
 (*Keep the full complexity of the original name*)
-fun flatten_name s = space_implode "_X" (NameSpace.unpack s);
+fun flatten_name s = space_implode "_X" (NameSpace.explode s);
 
 (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
   It returns a modified theory, unless skolemization fails.*)
diff -r f9d085c2625c -r 05f57309170c src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/res_clause.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -745,7 +745,7 @@
     val clss = conjectures @ axclauses
     val funcs = funcs_of_clauses clss arity_clauses
     and preds = preds_of_clauses clss classrel_clauses arity_clauses
-    and probname = Path.pack (Path.base (Path.unpack filename))
+    and probname = Path.implode (Path.base (Path.explode filename))
     val (axstrs, _) = ListPair.unzip (map clause2dfg axclauses)
     val tfree_clss = map dfg_tfree_clause (union_all tfree_litss) 
     val out = TextIO.openOut filename
diff -r f9d085c2625c -r 05f57309170c src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/res_hol_clause.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -578,7 +578,7 @@
 	val conjectures = make_conjecture_clauses thms
         val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses)
 	val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
-	and probname = Path.pack (Path.base (Path.unpack filename))
+	and probname = Path.implode (Path.base (Path.explode filename))
 	val axstrs = map (#1 o clause2dfg) axclauses'
 	val tfree_clss = map ResClause.dfg_tfree_clause (ResClause.union_all tfree_litss)
 	val out = TextIO.openOut filename
diff -r f9d085c2625c -r 05f57309170c src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/sat_solver.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -564,14 +564,14 @@
 	fun minisat_with_proofs fm =
 	let
 		val _          = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
-		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
-		val outpath    = File.tmp_path (Path.unpack "result")
-		val proofpath  = File.tmp_path (Path.unpack "result.prf")
-		val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.pack inpath) ^ " -r " ^ (Path.pack outpath) ^ " -t " ^ (Path.pack proofpath) ^ "> /dev/null"
+		val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
+		val outpath    = File.tmp_path (Path.explode "result")
+		val proofpath  = File.tmp_path (Path.explode "result.prf")
+		val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " -t " ^ (Path.implode proofpath) ^ "> /dev/null"
 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm
 		fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
-		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
-		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
+		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
+		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
 		val cnf        = PropLogic.defcnf fm
 		val result     = SatSolver.make_external_solver cmd writefn readfn cnf
 		val _          = try File.rm inpath
@@ -749,13 +749,13 @@
 	fun minisat fm =
 	let
 		val _          = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
-		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
-		val outpath    = File.tmp_path (Path.unpack "result")
-		val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.pack inpath) ^ " -r " ^ (Path.pack outpath) ^ " > /dev/null"
+		val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
+		val outpath    = File.tmp_path (Path.explode "result")
+		val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " > /dev/null"
 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
 		fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
-		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
-		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
+		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
+		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
 		val _          = try File.rm inpath
 		val _          = try File.rm outpath
@@ -788,7 +788,7 @@
 	  SatSolver.UNSATISFIABLE NONE =>
 		(let
 			(* string list *)
-			val proof_lines = ((split_lines o File.read) (Path.unpack "resolve_trace"))
+			val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace"))
 				handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
 			(* PropLogic.prop_formula -> int *)
 			fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
@@ -911,13 +911,13 @@
 		                    (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
 			(* both versions of zChaff appear to have the same interface, so we do *)
 			(* not actually need to distinguish between them in the following code *)
-		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
-		val outpath    = File.tmp_path (Path.unpack "result")
-		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
+		val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
+		val outpath    = File.tmp_path (Path.explode "result")
+		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
 		fun readfn ()  = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
-		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
-		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
+		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
+		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
 		val _          = try File.rm inpath
 		val _          = try File.rm outpath
@@ -936,13 +936,13 @@
 	fun berkmin fm =
 	let
 		val _          = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else ()
-		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
-		val outpath    = File.tmp_path (Path.unpack "result")
-		val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
+		val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
+		val outpath    = File.tmp_path (Path.explode "result")
+		val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
 		fun readfn ()  = SatSolver.read_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
-		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
-		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
+		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
+		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
 		val _          = try File.rm inpath
 		val _          = try File.rm outpath
@@ -961,13 +961,13 @@
 	fun jerusat fm =
 	let
 		val _          = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
-		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
-		val outpath    = File.tmp_path (Path.unpack "result")
-		val cmd        = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
+		val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
+		val outpath    = File.tmp_path (Path.explode "result")
+		val cmd        = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
 		fun readfn ()  = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
-		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
-		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
+		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
+		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
 		val _          = try File.rm inpath
 		val _          = try File.rm outpath
diff -r f9d085c2625c -r 05f57309170c src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/specification_package.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -128,8 +128,8 @@
         fun proc_single prop =
             let
                 val frees = Term.term_frees prop
-                val _ = assert (forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees)
-                               "Specificaton: Only free variables of sort 'type' allowed"
+                val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
+                  orelse error "Specificaton: Only free variables of sort 'type' allowed"
                 val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees)
             in
                 (prop_closed,frees)
@@ -145,8 +145,8 @@
         val (altcos,overloaded) = Library.split_list cos
         val (names,sconsts) = Library.split_list altcos
         val consts = map (term_of o Thm.read_cterm thy o rpair TypeInfer.logicT) sconsts
-        val _ = assert (not (Library.exists (not o Term.is_Const) consts))
-                       "Specification: Non-constant found as parameter"
+        val _ = not (Library.exists (not o Term.is_Const) consts)
+          orelse error "Specification: Non-constant found as parameter"
 
         fun proc_const c =
             let
diff -r f9d085c2625c -r 05f57309170c src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/General/file.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -7,8 +7,8 @@
 
 signature FILE =
 sig
-  val unpack_platform_path_fn: (string -> Path.T) ref
-  val unpack_platform_path: string -> Path.T
+  val explode_platform_path_fn: (string -> Path.T) ref
+  val explode_platform_path: string -> Path.T
   val platform_path_fn: (Path.T -> string) ref
   val platform_path: Path.T -> string
   val shell_path_fn: (Path.T -> string) ref
@@ -22,7 +22,7 @@
   eqtype info
   val info: Path.T -> info option
   val exists: Path.T -> bool
-  val assert: Path.T -> unit
+  val check: Path.T -> unit
   val rm: Path.T -> unit
   val mkdir: Path.T -> unit
   val read: Path.T -> string
@@ -41,20 +41,20 @@
 
 (* platform specific path representations *)
 
-val unpack_platform_path_fn = ref Path.unpack;
-fun unpack_platform_path s = ! unpack_platform_path_fn s;
+val explode_platform_path_fn = ref Path.explode;
+fun explode_platform_path s = ! explode_platform_path_fn s;
 
-val platform_path_fn = ref (Path.pack o Path.expand);
+val platform_path_fn = ref (Path.implode o Path.expand);
 fun platform_path path = ! platform_path_fn path;
 
-val shell_path_fn = ref (enclose "'" "'" o Path.pack o Path.expand);
+val shell_path_fn = ref (enclose "'" "'" o Path.implode o Path.expand);
 fun shell_path path = ! shell_path_fn path;
 
 
 (* current path *)
 
 val cd = Library.cd o platform_path;
-val pwd = unpack_platform_path o Library.pwd;
+val pwd = explode_platform_path o Library.pwd;
 
 fun norm_absolute p =
   let
@@ -94,9 +94,9 @@
 
 val exists = is_some o info;
 
-fun assert path =
+fun check path =
   if exists path then ()
-  else error ("No such file or directory: " ^ quote (Path.pack path));
+  else error ("No such file or directory: " ^ quote (Path.implode path));
 
 val rm = OS.FileSys.remove o platform_path;
 
@@ -137,12 +137,12 @@
     SOME ids => OS.FileSys.compare ids = EQUAL
   | NONE => false);
 
-fun copy from to = conditional (not (eq (from, to))) (fn () =>
-  let val target = if is_dir to then Path.append to (Path.base from) else to
-  in write target (read from) end);
+fun copy src dst = conditional (not (eq (src, dst))) (fn () =>
+  let val target = if is_dir dst then Path.append dst (Path.base src) else dst
+  in write target (read src) end);
 
-fun copy_dir from to = conditional (not (eq (from, to))) (fn () =>
-  (system_command ("cp -r -f " ^ shell_path from ^ "/. " ^ shell_path to); ()))
+fun copy_dir src dst = conditional (not (eq (src, dst))) (fn () =>
+  (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ()))
 
 
 (* use ML files *)
diff -r f9d085c2625c -r 05f57309170c src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/General/name_space.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -22,8 +22,8 @@
   val hidden: string -> string
   val separator: string                 (*single char*)
   val is_qualified: string -> bool
-  val pack: string list -> string
-  val unpack: string -> string list
+  val implode: string list -> string
+  val explode: string -> string list
   val append: string -> string -> string
   val qualified: string -> string -> string
   val base: string -> string
@@ -70,8 +70,8 @@
 val separator = ".";
 val is_qualified = exists_string (fn s => s = separator);
 
-val pack = space_implode separator;
-val unpack = space_explode separator;
+val implode_name = space_implode separator;
+val explode_name = space_explode separator;
 
 fun append name1 "" = name1
   | append "" name2 = name2
@@ -82,15 +82,15 @@
   else path ^ separator ^ name;
 
 fun base "" = ""
-  | base name = List.last (unpack name);
+  | base name = List.last (explode_name name);
 
 fun qualifier "" = ""
-  | qualifier name = pack (#1 (split_last (unpack name)));
+  | qualifier name = implode_name (#1 (split_last (explode_name name)));
 
 fun map_base _ "" = ""
   | map_base f name =
-      let val names = unpack name
-      in pack (nth_map (length names - 1) f names) end;
+      let val names = explode_name name
+      in implode_name (nth_map (length names - 1) f names) end;
 
 
 (* accesses *)
@@ -117,8 +117,8 @@
       [xs @ ys] @@ prefixes1 zs @@ [ws];
   in sfxs @ pfxs end;
 
-val accesses = map pack o suffixes_prefixes o unpack;
-val accesses' = map pack o Library.suffixes1 o unpack;
+val accesses = map implode_name o suffixes_prefixes o explode_name;
+val accesses' = map implode_name o Library.suffixes1 o explode_name;
 
 
 
@@ -228,10 +228,10 @@
   if is_hidden name then
     error ("Attempt to declare hidden name " ^ quote name)
   else
-    let val names = unpack name in
+    let val names = explode_name name in
       conditional (null names orelse exists (fn s => s = "") names) (fn () =>
         error ("Bad name declaration " ^ quote name));
-      fold (add_name name) (map pack (accs names)) space
+      fold (add_name name) (map implode_name (accs names)) space
     end;
 
 
@@ -258,7 +258,7 @@
 
 fun sticky_prefix prfx (Naming (path, (qualify, _))) =
   Naming (append path prfx,
-    (qualify, suffixes_prefixes_split (length (unpack path)) (length (unpack prfx))));
+    (qualify, suffixes_prefixes_split (length (explode_name path)) (length (explode_name prfx))));
 
 fun set_policy policy (Naming (path, _)) = Naming (path, policy);
 
@@ -284,6 +284,11 @@
 fun dest_table tab = map (apfst #1) (ext_table tab);
 fun extern_table tab = map (apfst #2) (ext_table tab);
 
+
+(*final declarations of this structure!*)
+val implode = implode_name;
+val explode = explode_name;
+
 end;
 
 structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
diff -r f9d085c2625c -r 05f57309170c src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/General/path.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -21,8 +21,8 @@
   val append: T -> T -> T
   val appends: T list -> T
   val make: string list -> T
-  val pack: T -> string
-  val unpack: string -> T
+  val implode: T -> string
+  val explode: string -> T
   val dir: T -> T
   val base: T -> T
   val ext: string -> T -> T
@@ -95,35 +95,35 @@
 fun norm path = rev_app [] path;
 
 
-(* pack *)
+(* implode *)
 
-fun pack_elem Root = ""
-  | pack_elem Parent = ".."
-  | pack_elem (Basic s) = s
-  | pack_elem (Variable s) = "$" ^ s;
+fun implode_elem Root = ""
+  | implode_elem Parent = ".."
+  | implode_elem (Basic s) = s
+  | implode_elem (Variable s) = "$" ^ s;
 
-fun pack (Path []) = "."
-  | pack (Path (Root :: xs)) = "/" ^ space_implode "/" (map pack_elem xs)
-  | pack (Path xs) = space_implode "/" (map pack_elem xs);
+fun implode_path (Path []) = "."
+  | implode_path (Path (Root :: xs)) = "/" ^ space_implode "/" (map implode_elem xs)
+  | implode_path (Path xs) = space_implode "/" (map implode_elem xs);
 
 
-(* unpack *)
+(* explode *)
 
-fun unpack_elem "" = Root
-  | unpack_elem ".." = Parent
-  | unpack_elem "~" = Variable "HOME"
-  | unpack_elem "~~" = Variable "ISABELLE_HOME"
-  | unpack_elem s =
+fun explode_elem "" = Root
+  | explode_elem ".." = Parent
+  | explode_elem "~" = Variable "HOME"
+  | explode_elem "~~" = Variable "ISABELLE_HOME"
+  | explode_elem s =
       (case explode s of
         "$" :: cs => variable_elem cs
       | cs => basic_elem cs);
 
-val unpack_elems = map unpack_elem o filter_out (fn c => c = "" orelse c = ".");
+val explode_elems = map explode_elem o filter_out (fn c => c = "" orelse c = ".");
 
-fun unpack str = Path (norm
+fun explode_path str = Path (norm
   (case space_explode "/" str of
-    "" :: ss => Root :: unpack_elems ss
-  | ss => unpack_elems ss));
+    "" :: ss => Root :: explode_elems ss
+  | ss => explode_elems ss));
 
 
 (* base element *)
@@ -131,7 +131,7 @@
 fun split_path f (path as Path xs) =
   (case try split_last xs of
     SOME (prfx, Basic s) => f (prfx, s)
-  | _ => error ("Cannot split path into dir/base: " ^ quote (pack path)));
+  | _ => error ("Cannot split path into dir/base: " ^ quote (implode_path path)));
 
 val dir = split_path (fn (prfx, _) => Path prfx);
 val base = split_path (fn (_, s) => Path [Basic s]);
@@ -150,10 +150,15 @@
 fun eval (Variable s) =
     (case getenv s of
       "" => error ("Undefined Isabelle environment variable: " ^ quote s)
-    | path => rep (unpack path))
+    | path => rep (explode_path path))
   | eval x = [x];
 
 val expand = rep #> maps eval #> norm #> Path;
-val position = expand #> pack #> quote #> Position.line_name 1;
+val position = expand #> implode_path #> quote #> Position.line_name 1;
+
+
+(*final declarations of this structure!*)
+val implode = implode_path;
+val explode = explode_path;
 
 end;
diff -r f9d085c2625c -r 05f57309170c src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/General/scan.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -42,8 +42,8 @@
   val one: ('a -> bool) -> 'a list -> 'a * 'a list
   val this: string list -> string list -> string list * string list
   val this_string: string -> string list -> string * string list
-  val any: ('a -> bool) -> 'a list -> 'a list * 'a list
-  val any1: ('a -> bool) -> 'a list -> 'a list * 'a list
+  val many: ('a -> bool) -> 'a list -> 'a list * 'a list
+  val many1: ('a -> bool) -> 'a list -> 'a list * 'a list
   val optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a
   val option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
   val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
@@ -143,12 +143,12 @@
 
 fun this_string s = this (explode s) >> K s;  (*primitive string -- no symbols here!*)
 
-fun any _ [] = raise MORE NONE
-  | any pred (lst as x :: xs) =
-      if pred x then apfst (cons x) (any pred xs)
+fun many _ [] = raise MORE NONE
+  | many pred (lst as x :: xs) =
+      if pred x then apfst (cons x) (many pred xs)
       else ([], lst);
 
-fun any1 pred = one pred -- any pred >> op ::;
+fun many1 pred = one pred -- many pred >> op ::;
 
 fun optional scan def = scan || succeed def;
 fun option scan = (scan >> SOME) || succeed NONE;
diff -r f9d085c2625c -r 05f57309170c src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/General/symbol.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -403,7 +403,7 @@
 
 (* scan *)
 
-val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode);
+val scan_id = Scan.one is_letter ^^ (Scan.many is_letdig >> implode);
 
 local
 
@@ -413,8 +413,8 @@
   $$ "\\" -- Scan.optional ($$ "\\") "" -- Scan.this_string "<^newline>" >> K "\n";
 
 val scan_raw =
-  Scan.this_string "raw:" ^^ (Scan.any raw_chr >> implode) ||
-  Scan.this_string "raw" ^^ (Scan.any1 is_ascii_digit >> implode);
+  Scan.this_string "raw:" ^^ (Scan.many raw_chr >> implode) ||
+  Scan.this_string "raw" ^^ (Scan.many1 is_ascii_digit >> implode);
 
 in
 
@@ -431,7 +431,7 @@
 (* source *)
 
 val recover =
-  Scan.any (fn s => not (is_blank s) andalso s <> "\"" andalso not_eof s) >> K [malformed];
+  Scan.many (fn s => not (is_blank s) andalso s <> "\"" andalso not_eof s) >> K [malformed];
 
 fun source do_recover src =
   Source.source stopper (Scan.bulk scan) (if do_recover then SOME recover else NONE) src;
diff -r f9d085c2625c -r 05f57309170c src/Pure/General/url.ML
--- a/src/Pure/General/url.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/General/url.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -13,8 +13,8 @@
     Http of string * Path.T |
     Ftp of string * Path.T
   val append: T -> T -> T
-  val pack: T -> string
-  val unpack: string -> T
+  val implode: T -> string
+  val explode: string -> T
 end;
 
 structure Url: URL =
@@ -38,26 +38,26 @@
   | append _ url = url;
 
 
-(* pack *)
+(* implode *)
 
-fun pack_path p = if Path.is_current p then "" else Path.pack p;
+fun implode_path p = if Path.is_current p then "" else Path.implode p;
 
-fun pack (File p) = pack_path p
-  | pack (RemoteFile (h, p)) = "file://" ^ h ^ pack_path p
-  | pack (Http (h, p)) = "http://" ^ h ^ pack_path p
-  | pack (Ftp (h, p)) = "ftp://" ^ h ^ pack_path p;
+fun implode_url (File p) = implode_path p
+  | implode_url (RemoteFile (h, p)) = "file://" ^ h ^ implode_path p
+  | implode_url (Http (h, p)) = "http://" ^ h ^ implode_path p
+  | implode_url (Ftp (h, p)) = "ftp://" ^ h ^ implode_path p;
 
 
-(* unpack *)
+(* explode *)
 
 local
 
 val scan_host =
-  (Scan.any1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
+  (Scan.many1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
   Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
 
-val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
-val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o implode o cons "/");
+val scan_path = Scan.many Symbol.not_eof >> (Path.explode o implode);
+val scan_path_root = Scan.many Symbol.not_eof >> (Path.explode o implode o cons "/");
 
 val scan_url =
   Scan.unless (Scan.this_string "file:" ||
@@ -71,8 +71,13 @@
 
 in
 
-fun unpack s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
+fun explode_url s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
 
 end;
 
+
+(*final declarations of this structure!*)
+val implode = implode_url;
+val explode = explode_url;
+
 end;
diff -r f9d085c2625c -r 05f57309170c src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/General/xml.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -118,7 +118,7 @@
 fun err s (xs, _) =
   "XML parsing error: " ^ s ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
 
-val scan_whspc = Scan.any Symbol.is_blank;
+val scan_whspc = Scan.many Symbol.is_blank;
 
 val scan_special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
 
diff -r f9d085c2625c -r 05f57309170c src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -192,7 +192,7 @@
 (* init and exit *)
 
 fun begin_theory name imports uses =
-  ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.unpack) uses);
+  ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.explode) uses);
 
 fun end_theory thy =
   if ThyInfo.check_known_thy (Context.theory_name thy) then ThyInfo.end_theory thy else thy;
@@ -298,7 +298,7 @@
 (* current working directory *)
 
 fun cd path = Toplevel.imperative (fn () => (File.cd path));
-val pwd = Toplevel.imperative (fn () => writeln (Path.pack (File.pwd ())));
+val pwd = Toplevel.imperative (fn () => writeln (Path.implode (File.pwd ())));
 
 
 (* load theory files *)
@@ -496,7 +496,7 @@
 (* markup commands *)
 
 fun add_header s = Toplevel.keep' (fn int => fn state =>
-  (Toplevel.assert (Toplevel.is_toplevel state);
+  (if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF;
    if int then OuterSyntax.check_text s NONE else ()));
 
 local
diff -r f9d085c2625c -r 05f57309170c src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Isar/isar_output.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -305,10 +305,10 @@
 local
 
 val space_proper =
-  Scan.one T.is_blank -- Scan.any T.is_comment -- Scan.one T.is_proper;
+  Scan.one T.is_blank -- Scan.many T.is_comment -- Scan.one T.is_proper;
 
 val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore);
-val improper = Scan.any is_improper;
+val improper = Scan.many is_improper;
 val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
 val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one T.is_blank));
 
@@ -375,7 +375,7 @@
     val cmd = Scan.one (is_some o fst);
     val non_cmd = Scan.one (is_none o fst andf not o #2 stopper) >> #2;
 
-    val comments = Scan.any (comment_token o fst o snd);
+    val comments = Scan.many (comment_token o fst o snd);
     val blank = Scan.one (blank_token o fst o snd);
     val newline = Scan.one (newline_token o fst o snd);
     val before_cmd =
diff -r f9d085c2625c -r 05f57309170c src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Isar/outer_lex.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -193,7 +193,7 @@
 val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
 
 val scan_symid =
-  Scan.any1 is_sym_char >> implode ||
+  Scan.many1 is_sym_char >> implode ||
   Scan.one Symbol.is_symbolic;
 
 fun is_symid str =
@@ -249,8 +249,8 @@
 fun is_space s = Symbol.is_blank s andalso s <> "\n";
 
 val scan_space =
-  (keep_line (Scan.any1 is_space) -- Scan.optional (incr_line ($$ "\n")) "" ||
-    keep_line (Scan.any is_space) -- incr_line ($$ "\n")) >> (fn (cs, c) => implode cs ^ c);
+  (keep_line (Scan.many1 is_space) -- Scan.optional (incr_line ($$ "\n")) "" ||
+    keep_line (Scan.many is_space) -- incr_line ($$ "\n")) >> (fn (cs, c) => implode cs ^ c);
 
 
 (* scan nested comments *)
@@ -303,7 +303,7 @@
 (* token sources *)
 
 val is_junk = (not o Symbol.is_blank) andf Symbol.not_sync andf Symbol.not_eof;
-fun recover xs = (keep_line (Scan.any is_junk) >> (fn ts => [malformed_of ts])) xs;
+fun recover xs = (keep_line (Scan.many is_junk) >> (fn ts => [malformed_of ts])) xs;
 
 fun source do_recover get_lex pos src =
   Source.source' pos Symbol.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
diff -r f9d085c2625c -r 05f57309170c src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -220,7 +220,7 @@
 val name = group "name declaration" (short_ident || sym_ident || string || number);
 val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
 val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
-val path = group "file name/path specification" name >> Path.unpack;
+val path = group "file name/path specification" name >> Path.explode;
 
 val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
 
diff -r f9d085c2625c -r 05f57309170c src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -253,9 +253,9 @@
     val ml_file = if ml andalso is_some (ThyLoad.check_file NONE ml_path) then [ml_path] else [];
   in
     if name <> name' then
-      error ("Filename " ^ quote (Path.pack path) ^
+      error ("Filename " ^ quote (Path.implode path) ^
         " does not agree with theory name " ^ quote name')
-    else (parents, map (Path.unpack o #1) files @ ml_file)
+    else (parents, map (Path.explode o #1) files @ ml_file)
   end;
 
 
@@ -268,7 +268,7 @@
     if is_none (ThyLoad.check_file NONE path) then ()
     else
       let
-        val _ = warning ("Loading legacy ML script " ^ quote (Path.pack path));
+        val _ = warning ("Loading legacy ML script " ^ quote (Path.implode path));
         val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
         val tr_name = if time then "time_use" else "use";
       in Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] end
diff -r f9d085c2625c -r 05f57309170c src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Isar/session.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -71,11 +71,11 @@
      if is_some (! remote_path) then
        error "Path for remote theory browsing information may only be set once"
      else
-       remote_path := SOME (Url.unpack rpath);
+       remote_path := SOME (Url.explode rpath);
    (! remote_path, rpath <> ""));
 
 fun dumping (_, "") = NONE
-  | dumping (cp, path) = SOME (cp, Path.unpack path);
+  | dumping (cp, path) = SOME (cp, Path.explode path);
 
 fun use_dir root build modes reset info doc doc_graph doc_versions
     parent name dump rpath level verbose =
diff -r f9d085c2625c -r 05f57309170c src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Proof/extraction.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -315,7 +315,7 @@
   in fn (thm, (vs, s1, s2)) =>
     let
       val name = Thm.get_name thm;
-      val _ = assert (name <> "") "add_realizers: unnamed theorem";
+      val _ = name <> "" orelse error "add_realizers: unnamed theorem";
       val prop = Pattern.rewrite_term thy'
         (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
       val vars = vars_of prop;
@@ -360,7 +360,7 @@
       defs, expand, prep} = ExtractionData.get thy;
 
     val name = Thm.get_name thm;
-    val _ = assert (name <> "") "add_expand_thms: unnamed theorem";
+    val _ = name <> "" orelse error "add_expand_thms: unnamed theorem";
 
     val is_def =
       (case strip_comb (fst (Logic.dest_equals (prop_of thm))) of
@@ -568,7 +568,7 @@
               NONE => (case find vs' (find' name defs') of
                 NONE =>
                   let
-                    val _ = assert (T = nullT) "corr: internal error";
+                    val _ = T = nullT orelse error "corr: internal error";
                     val _ = msg d ("Building correctness proof for " ^ quote name ^
                       (if null vs' then ""
                        else " (relevant variables: " ^ commas_quote vs' ^ ")"));
@@ -720,8 +720,8 @@
       let
         val {prop, der = (_, prf), sign, ...} = rep_thm thm;
         val name = Thm.get_name thm;
-        val _ = assert (name <> "") "extraction: unnamed theorem";
-        val _ = assert (etype_of thy' vs [] prop <> nullT) ("theorem " ^
+        val _ = name <> "" orelse error "extraction: unnamed theorem";
+        val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
           quote name ^ " has no computational content")
       in (Reconstruct.reconstruct_proof sign prop prf, vs) end;
 
diff -r f9d085c2625c -r 05f57309170c src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -134,16 +134,16 @@
     fun prf_of [] (Bound i) = PBound i
       | prf_of Ts (Const (s, Type ("proof", _))) =
           change_type (if ty then SOME Ts else NONE)
-            (case NameSpace.unpack s of
+            (case NameSpace.explode s of
                "axm" :: xs =>
                  let
-                   val name = NameSpace.pack xs;
+                   val name = NameSpace.implode xs;
                    val prop = (case AList.lookup (op =) axms name of
                        SOME prop => prop
                      | NONE => error ("Unknown axiom " ^ quote name))
                  in PAxm (name, prop, NONE) end
              | "thm" :: xs =>
-                 let val name = NameSpace.pack xs;
+                 let val name = NameSpace.implode xs;
                  in (case AList.lookup (op =) thms name of
                      SOME thm => fst (strip_combt (Thm.proof_of thm))
                    | NONE => (case Symtab.lookup tab name of
diff -r f9d085c2625c -r 05f57309170c src/Pure/ProofGeneral/pgip_output.ML
--- a/src/Pure/ProofGeneral/pgip_output.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/ProofGeneral/pgip_output.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -184,7 +184,7 @@
                   ("version", version),
                   ("instance", instance), 
                   ("descr", descr),
-                  ("url", Url.pack url),
+                  ("url", Url.implode url),
                   ("filenameextns", filenameextns)],
                  [])
     end
diff -r f9d085c2625c -r 05f57309170c src/Pure/ProofGeneral/pgip_types.ML
--- a/src/Pure/ProofGeneral/pgip_types.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/ProofGeneral/pgip_types.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -279,7 +279,7 @@
 (** Url operations **)
 
 fun pgipurl_of_string url = (* only handle file:/// or file://localhost/ *)
-	case Url.unpack url of
+	case Url.explode url of
             (Url.File path) => path
 	  | _ => raise PGIP ("Cannot access non-local URL " ^ url)
 		       
@@ -291,7 +291,7 @@
 val pgipurl_of_attrs = pgipurl_of_string o (get_attr "url")
 
 fun pgipurl_of_url (Url.File p) = p
-  | pgipurl_of_url url = raise PGIP ("Cannot access non-local/non-file URL " ^ (Url.pack url))
+  | pgipurl_of_url url = raise PGIP ("Cannot access non-local/non-file URL " ^ (Url.implode url))
 
 
 (** Messages and errors **)
diff -r f9d085c2625c -r 05f57309170c src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -176,7 +176,7 @@
 
 (* prepare theory context *)
 
-val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
+val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
 
 (* FIXME general treatment of tracing*)
 val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
@@ -187,7 +187,7 @@
   | NONE => "");
 
 fun try_update_thy_only file =
-  ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
+  ThyLoad.cond_add_path (Path.dir (Path.explode file)) (fn () =>
     let val name = thy_name file in
       if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name))
       then update_thy_only name
@@ -207,13 +207,13 @@
      (ThyInfo.touch_child_thys name;
       ThyInfo.pretend_use_thy_only name handle ERROR msg =>
        (warning msg; warning ("Failed to register theory: " ^ quote name);
-        tell_file_retracted (Path.base (Path.unpack file))))
+        tell_file_retracted (Path.base (Path.explode file))))
     else raise Toplevel.UNDEF
   end;
 
 fun vacuous_inform_file_processed file state =
  (warning ("No theory " ^ quote (thy_name file));
-  tell_file_retracted (Path.base (Path.unpack file)));
+  tell_file_retracted (Path.base (Path.explode file)));
 
 
 (* restart top-level loop (keeps most state information) *)
@@ -371,7 +371,7 @@
 
 fun write_keywords s =
  (init_outer_syntax ();
-  File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
+  File.write (Path.explode ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
     (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
 
 end;
diff -r f9d085c2625c -r 05f57309170c src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -271,7 +271,7 @@
 
 (* prepare theory context *)
 
-val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
+val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
 
 (* FIXME general treatment of tracing*)
 val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
@@ -282,7 +282,7 @@
   | NONE => "");
 
 fun try_update_thy_only file =
-  ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
+  ThyLoad.cond_add_path (Path.dir (Path.explode file)) (fn () =>
     let val name = thy_name file in
       if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name))
       then update_thy_only name
@@ -302,13 +302,13 @@
      (ThyInfo.touch_child_thys name;
       ThyInfo.pretend_use_thy_only name handle ERROR msg =>
        (warning msg; warning ("Failed to register theory: " ^ quote name);
-        tell_file_retracted (Path.base (Path.unpack file))))
+        tell_file_retracted (Path.base (Path.explode file))))
     else raise Toplevel.UNDEF
   end;
 
 fun vacuous_inform_file_processed file state =
  (warning ("No theory " ^ quote (thy_name file));
-  tell_file_retracted (Path.base (Path.unpack file)));
+  tell_file_retracted (Path.base (Path.explode file)));
 
 
 (* restart top-level loop (keeps most state information) *)
@@ -387,15 +387,15 @@
 in
 fun send_pgip_config () =
     let
-        val path = Path.unpack (config_file())
+        val path = Path.explode (config_file())
         val exists = File.exists path
 
 	val wwwpage = 
-	    (Url.unpack (isabelle_www()))
+	    (Url.explode (isabelle_www()))
 	    handle _ => 
 		   (Output.panic 
 			("Error in URL in environment variable ISABELLE_HOMEPAGE.");
-			Url.unpack isabellewww)
+			Url.explode isabellewww)
 		     
 	val proverinfo =
             Proverinfo { name = "Isabelle",
@@ -459,11 +459,11 @@
 
 fun use_thy_or_ml_file file =
     let
-        val (path,extn) = Path.split_ext (Path.unpack file)
+        val (path,extn) = Path.split_ext (Path.explode file)
     in
         case extn of
-            "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
-          | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
+            "" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
+          | "thy" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
           | "ML" => isarcmd ("use " ^ quote file)
           | other => error ("Don't know how to read a file with extension " ^ other)
     end
diff -r f9d085c2625c -r 05f57309170c src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/ROOT.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -99,7 +99,7 @@
 (*final ML setup*)
 use "install_pp.ML";
 val use = ThyInfo.use;
-val cd = File.cd o Path.unpack;
+val cd = File.cd o Path.explode;
 ml_prompts "ML> " "ML# ";
 
 proofs := 0;
diff -r f9d085c2625c -r 05f57309170c src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -93,10 +93,10 @@
 
 (** basic scanners **)
 
-val scan_letter_letdigs = Scan.one Symbol.is_letter -- Scan.any Symbol.is_letdig >> op ::;
-val scan_digits1 = Scan.any1 Symbol.is_digit;
-val scan_hex1 = Scan.any1 (Symbol.is_digit orf Symbol.is_hex_letter);
-val scan_bin1 = Scan.any1 (fn s => s = "0" orelse s = "1");
+val scan_letter_letdigs = Scan.one Symbol.is_letter -- Scan.many Symbol.is_letdig >> op ::;
+val scan_digits1 = Scan.many1 Symbol.is_digit;
+val scan_hex1 = Scan.many1 (Symbol.is_digit orf Symbol.is_hex_letter);
+val scan_bin1 = Scan.many1 (fn s => s = "0" orelse s = "1");
 
 val scan_id = scan_letter_letdigs >> implode;
 val scan_longid = scan_id ^^ (Scan.repeat1 ($$ "." ^^ scan_id) >> implode);
@@ -344,7 +344,7 @@
   let
     val scan =
       $$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol.is_eof) >> var ||
-      Scan.any Symbol.not_eof >> (free o implode);
+      Scan.many Symbol.not_eof >> (free o implode);
   in the (Scan.read Symbol.stopper scan (Symbol.explode str)) end;
 
 
@@ -388,7 +388,7 @@
 val ten = ord "0" + 10;
 val a = ord "a";
 val A = ord "A";
-val _ = assert (a > A) "Bad ASCII";
+val _ = a > A orelse error "Bad ASCII";
 
 fun remap_hex c =
   let val x = ord c in
@@ -421,8 +421,8 @@
 
 fun read_idents str =
   let
-    val blanks = Scan.any Symbol.is_blank;
-    val junk = Scan.any Symbol.not_eof;
+    val blanks = Scan.many Symbol.is_blank;
+    val junk = Scan.many Symbol.not_eof;
     val idents = Scan.repeat1 (blanks |-- scan_id --| blanks) -- junk;
   in
     (case Scan.read Symbol.stopper idents (Symbol.explode str) of
diff -r f9d085c2625c -r 05f57309170c src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -203,11 +203,11 @@
 val scan_sym =
   $$ "_" >> K (Argument ("", 0)) ||
   $$ "\\<index>" >> K index ||
-  $$ "(" |-- Scan.any Symbol.is_digit >> (Bg o read_int) ||
+  $$ "(" |-- Scan.many Symbol.is_digit >> (Bg o read_int) ||
   $$ ")" >> K En ||
   $$ "/" -- $$ "/" >> K (Brk ~1) ||
-  $$ "/" |-- Scan.any Symbol.is_blank >> (Brk o length) ||
-  Scan.any1 Symbol.is_blank >> (Space o implode) ||
+  $$ "/" |-- Scan.many Symbol.is_blank >> (Brk o length) ||
+  Scan.many1 Symbol.is_blank >> (Space o implode) ||
   Scan.repeat1 scan_delim_char >> (Delim o implode);
 
 val scan_symb =
diff -r f9d085c2625c -r 05f57309170c src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Thy/html.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -266,13 +266,13 @@
 val keyword = enclose "<span class=\"keyword\">" "</span>" o output;
 val keyword_width = apfst (enclose "<span class=\"keyword\">" "</span>") o output_width;
 val file_name = enclose "<span class=\"filename\">" "</span>" o output;
-val file_path = file_name o Url.pack;
+val file_path = file_name o Url.implode;
 
 
 (* misc *)
 
 fun href_name s txt = "<a href=" ^ Library.quote s ^ ">" ^ txt ^ "</a>";
-fun href_path path txt = href_name (Url.pack path) txt;
+fun href_path path txt = href_name (Url.implode path) txt;
 
 fun href_opt_name NONE txt = txt
   | href_opt_name (SOME s) txt = href_name s txt;
@@ -400,7 +400,7 @@
 (* ML file *)
 
 fun ml_file path str =
-  begin_document ("File " ^ Url.pack path) ^
+  begin_document ("File " ^ Url.implode path) ^
   "\n</div>\n<hr><div class=\"mlsource\">\n" ^
   verbatim str ^
   "\n</div>\n<hr>\n<div class=\"mlfooter\">\n" ^
diff -r f9d085c2625c -r 05f57309170c src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Thy/present.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -60,15 +60,15 @@
 val graph_eps_path = Path.basic "session_graph.eps";
 
 val session_path = Path.basic ".session";
-val session_entries_path = Path.unpack ".session/entries";
-val pre_index_path = Path.unpack ".session/pre-index";
+val session_entries_path = Path.explode ".session/entries";
+val pre_index_path = Path.explode ".session/pre-index";
 
 fun mk_rel_path [] ys = Path.make ys
   | mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent)
   | mk_rel_path (ps as x :: xs) (qs as y :: ys) = if x = y then mk_rel_path xs ys else
       Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
 
-fun show_path path = Path.pack (Path.append (File.pwd ()) path);
+fun show_path path = Path.implode (Path.append (File.pwd ()) path);
 
 
 
@@ -108,7 +108,7 @@
 fun display_graph gr =
   let
     val _ = writeln "Generating graph ...";
-    val path = File.tmp_path (Path.unpack "tmp.graph");
+    val path = File.tmp_path (Path.explode "tmp.graph");
     val _ = write_graph gr path;
     val _ = File.isatool ("browser -c " ^ File.shell_path path ^ " &");
   in () end;
@@ -126,9 +126,9 @@
     path =
       if null session then "" else
       if is_some remote_path andalso not is_local then
-        Url.pack (Url.append (the remote_path) (Url.File
+        Url.implode (Url.append (the remote_path) (Url.File
           (Path.append (Path.make session) (html_path name))))
-      else Path.pack (Path.append (mk_rel_path curr_sess session) (html_path name)),
+      else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)),
     unfold = false,
     parents =
       map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) (ThyInfo.get_preds name)}
@@ -271,7 +271,7 @@
 
 fun update_index dir name =
   (case try get_entries dir of
-    NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.pack dir))
+    NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.implode dir))
   | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir));
 
 
@@ -323,7 +323,7 @@
         (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
         map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
       val index_text = HTML.begin_index (index_up_lnk, parent_name)
-        (Url.File index_path, session_name) docs (Url.unpack "medium.html");
+        (Url.File index_path, session_name) docs (Url.explode "medium.html");
     in
       session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
       info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
@@ -407,10 +407,10 @@
       if length path > 1 then update_index parent_html_prefix name else ();
       (case readme of NONE => () | SOME path => File.copy path html_prefix);
       write_graph graph (Path.append html_prefix graph_path);
-      File.copy (Path.unpack "~~/lib/browser/GraphBrowser.jar") html_prefix;
+      File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
       List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
         (HTML.applet_pages name (Url.File index_path, name));
-      File.copy (Path.unpack "~~/lib/html/isabelle.css") html_prefix;
+      File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
       List.app finish_html thys;
       List.app (uncurry File.write) files;
       conditional verbose (fn () =>
@@ -474,7 +474,7 @@
               HTML.ml_file (Url.File base) (File.read path));
             (SOME (Url.File base_html), Url.File raw_path, loadit)
           end
-      | NONE => (warning ("Browser info: expected to find ML file" ^ quote (Path.pack raw_path));
+      | NONE => (warning ("Browser info: expected to find ML file" ^ quote (Path.implode raw_path));
           (NONE, Url.File raw_path, loadit)));
 
     val files_html = map prep_file files;
@@ -487,7 +487,7 @@
 
     val entry =
      {name = name, ID = ID_of path name, dir = sess_name, unfold = true,
-      path = Path.pack (html_path name),
+      path = Path.implode (html_path name),
       parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) raw_parents};
 
   in
@@ -523,11 +523,11 @@
       let
         val base = Path.base path;
         val name =
-          (case Path.pack (#1 (Path.split_ext base)) of "" => gensym "DUMMY" | s => s);
+          (case Path.implode (#1 (Path.split_ext base)) of "" => gensym "DUMMY" | s => s);
       in
         if File.exists path then
           (Buffer.add (Latex.theory_entry name) tex_index, (name, base, File.read path))
-        else error ("Bad file: " ^ quote (Path.pack path))
+        else error ("Bad file: " ^ quote (Path.implode path))
       end;
     val (tex_index, srcs) = foldl_map prep_draft (Buffer.empty, src_paths);
 
@@ -535,7 +535,7 @@
     val result_path = Path.append doc_path Path.parent;
     val _ = File.mkdir doc_path;
     val root_path = Path.append doc_path (Path.basic "root.tex");
-    val _ = File.copy (Path.unpack "~~/lib/texinputs/draft.tex") root_path;
+    val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path;
     val _ = File.isatool ("latex -o sty " ^ File.shell_path root_path);
     val _ = File.isatool ("latex -o syms " ^ File.shell_path root_path);
 
@@ -547,7 +547,7 @@
 
     val _ = srcs |> List.app (fn (name, base, txt) =>
       Symbol.explode txt
-      |> Latex.symbol_source (known_syms, known_ctrls) (Path.pack base)
+      |> Latex.symbol_source (known_syms, known_ctrls) (Path.implode base)
       |> File.write (Path.append doc_path (tex_path name)));
     val _ = write_tex_index tex_index doc_path;
   in isatool_document false doc_format documentN "" doc_path result_path end;
diff -r f9d085c2625c -r 05f57309170c src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Thy/thm_database.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -78,7 +78,7 @@
               NameSpace.intern space xname = name then
             SOME (prfx, (bname, xname, length (the (Symtab.lookup thms name)) = 1))
           else NONE;
-        val names = NameSpace.unpack name;
+        val names = NameSpace.explode name;
       in
         (case #2 (chop (length names - 2) names) of
           [bname] => result "" bname
diff -r f9d085c2625c -r 05f57309170c src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Thy/thm_deps.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -43,7 +43,7 @@
           if not (Symtab.defined gra name) then
             let
               val (gra', parents') = make_deps_graph prf' (gra, []);
-              val prefx = #1 (Library.split_last (NameSpace.unpack name));
+              val prefx = #1 (Library.split_last (NameSpace.explode name));
               val session =
                 (case prefx of
                   (x :: _) =>
diff -r f9d085c2625c -r 05f57309170c src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -256,7 +256,7 @@
 fun provide path name info (deps as SOME {present, outdated, master, files}) =
      (if exists (equal path o #1) files then ()
       else warning (loader_msg "undeclared dependency of theory" [name] ^
-        " on file: " ^ quote (Path.pack path));
+        " on file: " ^ quote (Path.implode path));
       SOME (make_deps present outdated master (AList.update (op =) (path, SOME info) files)))
   | provide _ _ _ NONE = NONE;
 
@@ -272,7 +272,7 @@
 
 fun load_file time path = Output.toplevel_errors (fn () =>
   if time then
-    let val name = Path.pack path in
+    let val name = Path.implode path in
       timeit (fn () =>
        (priority ("\n**** Starting file " ^ quote name ^ " ****");
         run_file path;
@@ -280,8 +280,8 @@
     end
   else run_file path) ();
 
-val use = load_file false o Path.unpack;
-val time_use = load_file true o Path.unpack;
+val use = load_file false o Path.explode;
+val time_use = load_file true o Path.explode;
 
 end;
 
@@ -303,7 +303,7 @@
       else #1 (ThyLoad.deps_thy dir name ml);
 
     val files = get_files name;
-    val missing_files = map_filter (fn (path, NONE) => SOME (Path.pack path) | _ => NONE) files;
+    val missing_files = map_filter (fn (path, NONE) => SOME (Path.implode path) | _ => NONE) files;
   in
     if null missing_files then ()
     else warning (loader_msg "unresolved dependencies of theory" [name] ^
@@ -315,7 +315,7 @@
 
 (* require_thy *)
 
-fun base_of_path s = Path.pack (Path.base (Path.unpack s));
+fun base_of_path s = Path.implode (Path.base (Path.explode s));
 
 local
 
@@ -333,7 +333,7 @@
   | SOME deps =>
       let
         fun get_name s = (case opt_path'' (lookup_deps s) of NONE => s
-          | SOME p => Path.pack (Path.append p (Path.basic s)));
+          | SOME p => Path.implode (Path.append p (Path.basic s)));
         val same_deps = (NONE, map get_name (thy_graph Graph.imm_preds name))
       in
         (case deps of
@@ -349,8 +349,8 @@
 
 fun require_thy really ml time strict keep_strict initiators prfx (visited, str) =
   let
-    val path = Path.expand (Path.unpack str);
-    val name = Path.pack (Path.base path);
+    val path = Path.expand (Path.explode str);
+    val name = Path.implode (Path.base path);
   in
     if member (op =) initiators name then error (cycle_msg initiators) else ();
     if known_thy name andalso is_finished name orelse member (op =) visited name then
@@ -422,7 +422,7 @@
   let val illegal = map (fn ext => Path.ext ext (Path.basic name)) ThyLoad.ml_exts in
     (case find_first (member (op =) illegal o Path.base o Path.expand o #1) uses of
       NONE => ()
-    | SOME (path, _) => error ("Illegal use of theory ML file: " ^ quote (Path.pack path)))
+    | SOME (path, _) => error ("Illegal use of theory ML file: " ^ quote (Path.implode path)))
   end;
 
 fun begin_theory present name parents uses int =
diff -r f9d085c2625c -r 05f57309170c src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Thy/thy_load.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -49,12 +49,12 @@
 val load_path = ref [Path.current];
 fun change_path f = load_path := f (! load_path);
 
-fun show_path () = map Path.pack (! load_path);
-fun del_path s = change_path (filter_out (equal (Path.unpack s)));
-fun add_path s = (del_path s; change_path (cons (Path.unpack s)));
-fun path_add s = (del_path s; change_path (fn path => path @ [Path.unpack s]));
+fun show_path () = map Path.implode (! load_path);
+fun del_path s = change_path (filter_out (equal (Path.explode s)));
+fun add_path s = (del_path s; change_path (cons (Path.explode s)));
+fun path_add s = (del_path s; change_path (fn path => path @ [Path.explode s]));
 fun reset_path () = load_path := [Path.current];
-fun with_paths ss f x = Library.setmp load_path (! load_path @ map Path.unpack ss) f x;
+fun with_paths ss f x = Library.setmp load_path (! load_path @ map Path.explode ss) f x;
 fun with_path s f x = with_paths [s] f x;
 
 fun cond_add_path path f x =
@@ -95,7 +95,7 @@
 
 fun load_file current raw_path =
   (case check_file current raw_path of
-    NONE => error ("Could not find ML file " ^ quote (Path.pack raw_path))
+    NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))
   | SOME (path, info) => (File.use path; (path, info)));
 
 
@@ -113,7 +113,7 @@
 fun check_thy_aux (name, ml) =
   let val thy_file = thy_path name in
     case check_file NONE thy_file of
-      NONE => error ("Could not find theory file " ^ quote (Path.pack thy_file) ^
+      NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^
         " in dir(s) " ^ commas_quote (show_path ()))
     | SOME thy_info => (thy_info, if ml then check_file NONE (ml_path name) else NONE)
   end;
diff -r f9d085c2625c -r 05f57309170c src/Pure/Tools/codegen_names.ML
--- a/src/Pure/Tools/codegen_names.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Tools/codegen_names.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -176,12 +176,12 @@
   let
     fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
     val is_junk = not o is_valid andf Symbol.not_eof;
-    val junk = Scan.any is_junk;
+    val junk = Scan.many is_junk;
     val scan_valids = Symbol.scanner "Malformed input"
       ((junk |--
-        (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.any is_valid >> implode)
+        (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
         --| junk))
-      -- Scan.repeat ((Scan.any1 is_valid >> implode) --| junk) >> op ::);
+      -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::);
   in explode #> scan_valids #> space_implode "_" end;
 
 fun purify_op "0" = "zero"
@@ -212,11 +212,11 @@
 
 fun check_modulename mn =
   let
-    val mns = NameSpace.unpack mn;
+    val mns = NameSpace.explode mn;
     val mns' = map purify_upper mns;
   in
     if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
-      ^ "perhaps try " ^ quote (NameSpace.pack mns'))
+      ^ "perhaps try " ^ quote (NameSpace.implode mns'))
   end
 
 fun purify_var "" = "x"
@@ -234,9 +234,9 @@
 
 fun policy thy get_basename get_thyname name =
   let
-    val prefix = (purify_prefix o NameSpace.unpack o get_thyname thy) name;
+    val prefix = (purify_prefix o NameSpace.explode o get_thyname thy) name;
     val base = (purify_base o get_basename) name;
-  in NameSpace.pack (prefix @ [base]) end;
+  in NameSpace.implode (prefix @ [base]) end;
 
 fun class_policy thy = policy thy NameSpace.base thyname_of_class;
 fun tyco_policy thy = policy thy NameSpace.base thyname_of_tyco;
@@ -258,10 +258,10 @@
   case force_thyname thy (c, tys)
    of NONE => policy thy NameSpace.base thyname_of_const c
     | SOME thyname => let
-        val prefix = (purify_prefix o NameSpace.unpack) thyname;
+        val prefix = (purify_prefix o NameSpace.explode) thyname;
         val tycos = map_filter (fn Type (tyco, _) => SOME tyco | _ => NONE) tys;
         val base = map (purify_base o NameSpace.base) (c :: tycos);
-      in NameSpace.pack (prefix @ [space_implode "_" base]) end;
+      in NameSpace.implode (prefix @ [space_implode "_" base]) end;
 
 
 (* shallow name spaces *)
@@ -274,20 +274,20 @@
 
 fun add_nsp shallow name =
   name
-  |> NameSpace.unpack
+  |> NameSpace.explode
   |> split_last
   |> apsnd (single #> cons shallow)
   |> (op @)
-  |> NameSpace.pack;
+  |> NameSpace.implode;
 
 fun dest_nsp nsp nspname =
   let
-    val xs = NameSpace.unpack nspname;
+    val xs = NameSpace.explode nspname;
     val (ys, base) = split_last xs;
     val (module, shallow) = split_last ys;
   in
     if nsp = shallow
-   then (SOME o NameSpace.pack) (module @ [base])
+   then (SOME o NameSpace.implode) (module @ [base])
     else NONE
   end;
 
diff -r f9d085c2625c -r 05f57309170c src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -235,7 +235,7 @@
 
 fun dest_name name =
   let
-    val (names, name_base) = (split_last o NameSpace.unpack) name;
+    val (names, name_base) = (split_last o NameSpace.explode) name;
     val (names_mod, name_shallow) = split_last names;
   in (names_mod, (name_shallow, name_base)) end;
 
@@ -257,7 +257,7 @@
     fun dictvar v = 
       first_upper v ^ "_";
     val label = translate_string (fn "." => "__" | c => c)
-      o NameSpace.pack o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.unpack;
+      o NameSpace.implode o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.explode;
     fun pr_tyvar (v, []) =
           str "()"
       | pr_tyvar (v, sort) =
@@ -584,7 +584,7 @@
     fun dictvar v = 
       first_upper v ^ "_";
     val label = translate_string (fn "." => "__" | c => c)
-      o NameSpace.pack o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.unpack;
+      o NameSpace.implode o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.explode;
     fun pr_tyvar (v, []) =
           str "()"
       | pr_tyvar (v, sort) =
@@ -924,9 +924,9 @@
     val init_vars = CodegenThingol.make_vars (ML_Syntax.reserved_names @ reserved_user);
     fun name_modl modl =
       let
-        val modlname = NameSpace.pack modl
+        val modlname = NameSpace.implode modl
       in case module_alias modlname
-       of SOME modlname' => NameSpace.unpack modlname'
+       of SOME modlname' => NameSpace.explode modlname'
         | NONE => map (fn name => (the_single o fst)
             (Name.variants [name] empty_names)) modl
       end;
@@ -992,14 +992,14 @@
             val (modl'', defname'') = (apfst name_modl o dest_name) name'';
           in if modl' = modl'' then
             map_node modl'
-              (Graph.add_edge (NameSpace.pack (modl @ [fst defname, snd defname]), name''))
+              (Graph.add_edge (NameSpace.implode (modl @ [fst defname, snd defname]), name''))
           else let
             val (common, (diff1::_, diff2::_)) = chop_prefix (op =) (modl', modl'');
           in
             map_node common
               (fn gr => Graph.add_edge_acyclic (diff1, diff2) gr
                 handle Graph.CYCLES _ => error ("Dependency "
-                  ^ quote (NameSpace.pack (modl' @ [fst defname, snd defname]))
+                  ^ quote (NameSpace.implode (modl' @ [fst defname, snd defname]))
                   ^ " -> " ^ quote name'' ^ " would result in module dependency cycle"))
           end end;
       in
@@ -1039,7 +1039,7 @@
           |> fold (fn m => fn g => case Graph.get_node g m
               of Module (_, (_, g)) => g) modl'
           |> (fn g => case Graph.get_node g name of Def (defname, _) => defname);
-      in NameSpace.pack (remainder @ [defname']) end handle Graph.UNDEF _ =>
+      in NameSpace.implode (remainder @ [defname']) end handle Graph.UNDEF _ =>
         "(raise Fail \"undefined name " ^ name ^ "\")";
     fun the_prolog modlname = case module_prolog modlname
      of NONE => []
@@ -1049,7 +1049,7 @@
       | pr_node prefix (Def (_, SOME def)) =
           SOME (pr_def tyco_syntax const_syntax init_vars (deresolver prefix) def)
       | pr_node prefix (Module (dmodlname, (_, nodes))) =
-          SOME (pr_modl dmodlname (the_prolog (NameSpace.pack (prefix @ [dmodlname]))
+          SOME (pr_modl dmodlname (the_prolog (NameSpace.implode (prefix @ [dmodlname]))
             @ separate (str "") ((map_filter (pr_node (prefix @ [dmodlname]) o Graph.get_node nodes)
                 o rev o flat o Graph.strong_conn) nodes)));
     val p = pr_modl "ROOT" (the_prolog "" @ separate (str "") ((map_filter
@@ -1058,7 +1058,7 @@
 
 val isar_seri_sml =
   let
-    fun output_file file p = File.write (Path.unpack file) (Pretty.output p ^ "\n");
+    fun output_file file p = File.write (Path.explode file) (Pretty.output p ^ "\n");
     fun output_diag p = Pretty.writeln p;
     fun output_internal p = use_text Output.ml_output false (Pretty.output p);
   in
@@ -1070,7 +1070,7 @@
 
 val isar_seri_ocaml =
   let
-    fun output_file file p = File.write (Path.unpack file) (Pretty.output p ^ "\n");
+    fun output_file file p = File.write (Path.explode file) (Pretty.output p ^ "\n");
     fun output_diag p = Pretty.writeln p;
   in
     parse_args ((Args.$$$ "-" >> K output_diag
@@ -1330,16 +1330,16 @@
 fun seri_haskell module_prefix destination string_classes reserved_user module_alias module_prolog
   class_syntax tyco_syntax const_syntax code =
   let
-    val _ = Option.map File.assert destination;
+    val _ = Option.map File.check destination;
     val empty_names = Name.make_context (reserved_haskell @ reserved_user);
     fun name_modl modl =
       let
-        val modlname = NameSpace.pack modl
+        val modlname = NameSpace.implode modl
       in (modlname, case module_alias modlname
        of SOME modlname' => (case module_prefix
             of NONE => modlname'
              | SOME module_prefix => NameSpace.append module_prefix modlname')
-        | NONE => NameSpace.pack (map_filter I (module_prefix :: map (fn name => (SOME o the_single o fst)
+        | NONE => NameSpace.implode (map_filter I (module_prefix :: map (fn name => (SOME o the_single o fst)
             (Name.variants [name] empty_names)) modl)))
       end;
     fun add_def (name, (def, deps)) =
@@ -1409,8 +1409,8 @@
     fun write_module (SOME destination) modlname p =
           let
             val filename = case modlname
-             of "" => Path.unpack "Main.hs"
-              | _ => (Path.ext "hs" o Path.unpack o implode o separate "/" o NameSpace.unpack) modlname;
+             of "" => Path.explode "Main.hs"
+              | _ => (Path.ext "hs" o Path.explode o implode o separate "/" o NameSpace.explode) modlname;
             val pathname = Path.append destination filename;
             val _ = File.mkdir (Path.dir pathname);
           in File.write pathname (Pretty.setmp_margin 999999 Pretty.output p ^ "\n") end
@@ -1435,7 +1435,7 @@
     -- Scan.optional (Args.$$$ "string_classes" >> K true) false
     -- (Args.$$$ "-" >> K NONE || Args.name >> SOME)
     >> (fn ((module_prefix, string_classes), destination) =>
-      seri_haskell module_prefix (Option.map Path.unpack destination) string_classes));
+      seri_haskell module_prefix (Option.map Path.explode destination) string_classes));
 
 
 (** diagnosis serializer **)
diff -r f9d085c2625c -r 05f57309170c src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/codegen.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -443,7 +443,7 @@
             | (true, "isup") => "" :: check_str zs
             | (ctrl, s') => (if ctrl then "ctrl_" ^ s' else s') :: check_str zs)
         | (ys, zs) => implode ys :: check_str zs);
-    val s' = space_implode "_" (maps (check_str o Symbol.explode) (NameSpace.unpack s))
+    val s' = space_implode "_" (maps (check_str o Symbol.explode) (NameSpace.explode s))
   in
     if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s'
   end;
@@ -453,7 +453,7 @@
     fun find_name [] = sys_error "mk_long_id"
       | find_name (ys :: yss) =
           let
-            val s' = NameSpace.pack ys
+            val s' = NameSpace.implode ys
             val s'' = NameSpace.append module s'
           in case Symtab.lookup used s'' of
               NONE => ((module, s'),
@@ -462,7 +462,7 @@
             | SOME _ => find_name yss
           end
   in case Symtab.lookup tab s of
-      NONE => find_name (Library.suffixes1 (NameSpace.unpack s))
+      NONE => find_name (Library.suffixes1 (NameSpace.explode s))
     | SOME name => (name, p)
   end;
 
@@ -874,9 +874,9 @@
 fun gen_generate_code prep_term thy modules module =
   setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs =>
   let
-    val _ = assert (module <> "" orelse
+    val _ = (module <> "" orelse
         member (op =) (!mode) "library" andalso forall (equal "" o fst) xs)
-      "missing module name";
+      orelse error "missing module name";
     val graphs = get_modules thy;
     val defs = mk_deftab thy;
     val gr = new_node ("<Top>", (NONE, module, ""))
@@ -958,10 +958,10 @@
 
 fun test_term thy sz i t =
   let
-    val _ = assert (null (term_tvars t) andalso null (term_tfrees t))
-      "Term to be tested contains type variables";
-    val _ = assert (null (term_vars t))
-      "Term to be tested contains schematic variables";
+    val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
+      error "Term to be tested contains type variables";
+    val _ = null (term_vars t) orelse
+      error "Term to be tested contains schematic variables";
     val frees = map dest_Free (term_frees t);
     val frees' = frees ~~
       map (fn i => "arg" ^ string_of_int i) (1 upto length frees);
@@ -1028,10 +1028,10 @@
 
 fun eval_term thy = setmp print_mode [] (fn t =>
   let
-    val _ = assert (null (term_tvars t) andalso null (term_tfrees t))
-      "Term to be evaluated contains type variables";
-    val _ = assert (null (term_vars t) andalso null (term_frees t))
-      "Term to be evaluated contains variables";
+    val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
+      error "Term to be evaluated contains type variables";
+    val _ = (null (term_vars t) andalso null (term_frees t)) orelse
+      error "Term to be evaluated contains variables";
     val (code, gr) = setmp mode ["term_of"]
       (generate_code_i thy [] "Generated") [("result", t)];
     val s = "structure EvalTerm =\nstruct\n\n" ^
@@ -1155,10 +1155,10 @@
        | SOME fname =>
            if lib then
              app (fn (name, s) => File.write
-                 (Path.append (Path.unpack fname) (Path.basic (name ^ ".ML"))) s)
+                 (Path.append (Path.explode fname) (Path.basic (name ^ ".ML"))) s)
                (("ROOT", implode (map (fn (name, _) =>
                    "use \"" ^ name ^ ".ML\";\n") code)) :: code)
-           else File.write (Path.unpack fname) (snd (hd code)));
+           else File.write (Path.explode fname) (snd (hd code)));
            if lib then thy
            else map_modules (Symtab.update (module, gr)) thy)
      end));
diff -r f9d085c2625c -r 05f57309170c src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/proof_general.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -402,7 +402,7 @@
 
 (* prepare theory context *)
 
-val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
+val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
 
 (* FIXME general treatment of tracing*)
 val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
@@ -413,7 +413,7 @@
   | NONE => "");
 
 fun try_update_thy_only file =
-  ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
+  ThyLoad.cond_add_path (Path.dir (Path.explode file)) (fn () =>
     let val name = thy_name file in
       if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name))
       then update_thy_only name
@@ -433,13 +433,13 @@
      (ThyInfo.touch_child_thys name;
       ThyInfo.pretend_use_thy_only name handle ERROR msg =>
        (warning msg; warning ("Failed to register theory: " ^ quote name);
-        tell_file_retracted (Path.base (Path.unpack file))))
+        tell_file_retracted (Path.base (Path.explode file))))
     else raise Toplevel.UNDEF
   end;
 
 fun vacuous_inform_file_processed file state =
  (warning ("No theory " ^ quote (thy_name file));
-  tell_file_retracted (Path.base (Path.unpack file)));
+  tell_file_retracted (Path.base (Path.explode file)));
 
 
 (* restart top-level loop (keeps most state information) *)
@@ -653,7 +653,7 @@
 in
 fun send_pgip_config () =
     let
-        val path = Path.unpack (config_file())
+        val path = Path.explode (config_file())
         val exists = File.exists path
         val proverinfo =
             XML.element "proverinfo"
@@ -678,7 +678,7 @@
 fun send_informguise (openfile, opentheory, openproofpos) =
     let val guisefile =
             case openfile of SOME f => [XML.element "guisefile"
-                                                    [("url",Url.pack (Url.File (Path.unpack f)))] []]
+                                                    [("url",Url.implode (Url.File (Path.explode f)))] []]
                            | _ => []
         val guisetheory =
             case opentheory of SOME t => [XML.element "guisetheory" [("thyname", t)] []]
@@ -1172,11 +1172,11 @@
 
 fun use_thy_or_ml_file file =
     let
-        val (path,extn) = Path.split_ext (Path.unpack file)
+        val (path,extn) = Path.split_ext (Path.explode file)
     in
         case extn of
-            "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
-          | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
+            "" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
+          | "thy" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
           | "ML" => isarcmd ("use " ^ quote file)
           | other => error ("Don't know how to read a file with extension " ^ other)
     end
@@ -1199,7 +1199,7 @@
   val name_attr = xmlattr "name"
 
   fun localfile_of_url url = (* only handle file:/// or file://localhost/ *)
-      case Url.unpack url of
+      case Url.explode url of
           (Url.File path) => File.platform_path path
         | _ => error ("Cannot access non-local URL " ^ url)
 
@@ -1515,7 +1515,7 @@
 
 fun write_keywords s =
  (init_outer_syntax ();
-  File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
+  File.write (Path.explode ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
     (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
 
 end;
diff -r f9d085c2625c -r 05f57309170c src/Pure/type.ML
--- a/src/Pure/type.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/type.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -535,7 +535,8 @@
 fun map_types f = map_tsig (fn (classes, default, types) =>
   let
     val (space', tab') = f types;
-    val _ = assert (NameSpace.intern space' "dummy" = "dummy") "Illegal declaration of dummy type";
+    val _ = NameSpace.intern space' "dummy" = "dummy" orelse
+      error "Illegal declaration of dummy type";
   in (classes, default, (space', tab')) end);
 
 fun syntactic types (Type (c, Ts)) =