# HG changeset patch
# User wenzelm
# Date 1116317984 -7200
# Node ID 5fd94d84470f361942efcde8a017d37ffb074049
# Parent  8ac3803c8f73688afb2c9039d9ce0e98a754f23e
tuned;

diff -r 8ac3803c8f73 -r 5fd94d84470f NEWS
--- a/NEWS	Tue May 17 10:19:43 2005 +0200
+++ b/NEWS	Tue May 17 10:19:44 2005 +0200
@@ -6,41 +6,6 @@
 
 *** General ***
 
-* ML: The type Library.option is no more, along with the exception
-  Library.OPTION: Isabelle now uses the standard option type.  The
-  functions the, is_some, is_none, etc. are still in Library, but
-  the constructors are now SOME and NONE instead of Some and None.
-  They raise the exception Option.
-
-* ML: The exception LIST is no more, the standard exceptions Empty and
-  Subscript, as well as Library.UnequalLengths are used instead.  This
-  means that function like Library.hd and Library.tl are gone, as the
-  standard hd and tl functions suffice.
-
-  A number of basic functions are now no longer exported to the top ML
-  level, as they are variants of standard functions.  The following
-  suggests how one can translate existing code:
-
-    the x = valOf x
-    if_none x y = getOpt(x,y)
-    is_some x = isSome x
-    apsome f x = Option.map f x
-    rev_append xs ys = List.revAppend(xs,ys)
-    nth_elem(i,xs) = List.nth(xs,i)
-    last_elem xs = List.last xs
-    flat xss = List.concat xss
-    seq fs = app fs
-    partition P xs = List.partition P xs
-    filter P xs = List.filter P xs
-    mapfilter f xs = List.mapPartial f xs
-
-  The final four functions, take, drop, foldl, and foldr, are somewhat
-  more complicated (especially the semantics of take and drop differ
-  from the standard).
-
-  A simple solution to broken code is to include "open Library" at the
-  beginning of a structure.  Everything after that will be as before.
-
 * Theory headers: the new header syntax for Isar theories is
 
   theory <name>
@@ -381,6 +346,30 @@
 
 *** ML ***
 
+* Pure/library.ML no longer defines its own option datatype, but uses
+  that of the SML basis, which has constructors NONE and SOME instead
+  of None and Some, as well as exception Option.Option instead of
+  OPTION.  The functions the, if_none, is_some, is_none have been
+  adapted accordingly, while Option.map replaces apsome.
+
+* The exception LIST is no more, the standard exceptions Empty and
+  Subscript, as well as Library.UnequalLengths are used instead.  This
+  means that function like Library.hd and Library.tl are gone, as the
+  standard hd and tl functions suffice.
+
+  A number of basic functions are now no longer exported to the ML
+  toplevel, as they are variants of standard functions.  The following
+  suggests how one can translate existing code:
+
+    rev_append xs ys = List.revAppend (xs, ys)
+    nth_elem (i, xs) = List.nth (xs, i)
+    last_elem xs = List.last xs
+    flat xss = List.concat xss
+    seq fs = app fs
+    partition P xs = List.partition P xs
+    filter P xs = List.filter P xs
+    mapfilter f xs = List.mapPartial f xs
+
 * Pure: output via the Isabelle channels of writeln/warning/error
   etc. is now passed through Output.output, with a hook for arbitrary
   transformations depending on the print_mode (cf. Output.add_mode --
diff -r 8ac3803c8f73 -r 5fd94d84470f src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue May 17 10:19:43 2005 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue May 17 10:19:44 2005 +0200
@@ -241,10 +241,10 @@
 
 fun error_var msg xi = error (msg ^ Syntax.string_of_vname xi);
 
-fun the_sort sorts xi = valOf (sorts xi)
+fun the_sort sorts xi = the (sorts xi)
   handle Option.Option => error_var "No such type variable in theorem: " xi;
 
-fun the_type types xi = valOf (types xi)
+fun the_type types xi = the (types xi)
   handle Option.Option => error_var "No such variable in theorem: " xi;
 
 fun unify_types sign types ((unifier, maxidx), (xi, u)) =
@@ -339,9 +339,9 @@
 
     mixed_insts |> List.app (fn (arg, (xi, _)) =>
       if is_tvar xi then
-        Args.assign (SOME (Args.Typ (valOf (assoc (type_insts''', xi))))) arg
+        Args.assign (SOME (Args.Typ (the (assoc (type_insts''', xi))))) arg
       else
-        Args.assign (SOME (Args.Term (valOf (assoc (term_insts''', xi))))) arg);
+        Args.assign (SOME (Args.Term (the (assoc (term_insts''', xi))))) arg);
 
     (context, thm''' |> RuleCases.save thm)
   end;
diff -r 8ac3803c8f73 -r 5fd94d84470f src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Tue May 17 10:19:43 2005 +0200
+++ b/src/Pure/Isar/calculation.ML	Tue May 17 10:19:44 2005 +0200
@@ -189,7 +189,7 @@
       | SOME calc => (false, Seq.map single (combine (calc @ facts))));
   in
     err_if state (initial andalso final) "No calculation yet";
-    err_if state (initial andalso isSome opt_rules) "Initial calculation -- no rules to be given";
+    err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
     calculations |> Seq.map (fn calc => (print (Proof.context_of state) calc;
         state |> maintain_calculation final calc))
   end;
diff -r 8ac3803c8f73 -r 5fd94d84470f src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Tue May 17 10:19:43 2005 +0200
+++ b/src/Pure/Isar/context_rules.ML	Tue May 17 10:19:44 2005 +0200
@@ -111,7 +111,7 @@
 fun print_rules prt x (Rules {rules, ...}) =
   let
     fun prt_kind (i, b) =
-      Pretty.big_list (valOf (assoc (kind_names, (i, b))) ^ ":")
+      Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":")
         (List.mapPartial (fn (_, (k, th)) => if k = (i, b) then SOME (prt x th) else NONE)
           (sort (Int.compare o pairself fst) rules));
   in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
diff -r 8ac3803c8f73 -r 5fd94d84470f src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue May 17 10:19:43 2005 +0200
+++ b/src/Pure/Isar/method.ML	Tue May 17 10:19:44 2005 +0200
@@ -154,7 +154,7 @@
 (* shuffle *)
 
 fun prefer i = METHOD (K (Tactic.defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1)));
-fun defer opt_i = METHOD (K (Tactic.defer_tac (getOpt (opt_i,1))));
+fun defer opt_i = METHOD (K (Tactic.defer_tac (if_none opt_i 1)));
 
 
 (* insert *)
@@ -263,7 +263,7 @@
 in
 
 fun rules_tac ctxt opt_lim =
-  SELECT_GOAL (DEEPEN (2, getOpt (opt_lim,20)) (intpr_tac ctxt [] 0) 4 1);
+  SELECT_GOAL (DEEPEN (2, if_none opt_lim 20) (intpr_tac ctxt [] 0) 4 1);
 
 end;
 
@@ -376,12 +376,12 @@
                 NONE => types (a, ~1)
               | some => some)
           | types' xi = types xi;
-        fun internal x = isSome (types' (x, ~1));
+        fun internal x = is_some (types' (x, ~1));
         val used = Drule.add_used thm (Drule.add_used st []);
         val (ts, envT) =
           ProofContext.read_termTs_schematic ctxt internal types' sorts used (ss ~~ Ts);
         val envT' = map (fn (ixn, T) =>
-          (TVar (ixn, valOf (rsorts ixn)), T)) envT @ Tinsts_env;
+          (TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env;
         val cenv =
           map
             (fn (xi, t) =>
@@ -735,7 +735,7 @@
 fun proof opt_text state =
   state
   |> Proof.assert_backward
-  |> refine (getOpt (opt_text,default_text))
+  |> refine (if_none opt_text default_text)
   |> Seq.map (Proof.goal_facts (K []))
   |> Seq.map Proof.enter_forward;
 
diff -r 8ac3803c8f73 -r 5fd94d84470f src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Tue May 17 10:19:43 2005 +0200
+++ b/src/Pure/Isar/object_logic.ML	Tue May 17 10:19:44 2005 +0200
@@ -47,7 +47,7 @@
 
   fun merge_judgment (SOME x, SOME y) =
         if x = y then SOME x else error "Attempt to merge different object-logics"
-    | merge_judgment (j1, j2) = if isSome j1 then j1 else j2;
+    | merge_judgment (j1, j2) = if is_some j1 then j1 else j2;
 
   fun merge ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
     (merge_judgment (judgment1, judgment2),
@@ -117,7 +117,7 @@
     val c = judgment_name sg;
     val aT = TFree ("'a", []);
     val T =
-      getOpt (Sign.const_type sg c, aT --> propT)
+      if_none (Sign.const_type sg c) (aT --> propT)
       |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
     val U = Term.domain_type T handle Match => aT;
   in Const (c, T) $ Free (x, U) end;
diff -r 8ac3803c8f73 -r 5fd94d84470f src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue May 17 10:19:43 2005 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue May 17 10:19:44 2005 +0200
@@ -280,7 +280,7 @@
   Source.of_list toks
   |> toplevel_source false true true get_parser
   |> Source.exhaust
-  |> map (fn tr => (Toplevel.name_of tr, valOf (Toplevel.source_of tr), tr));
+  |> map (fn tr => (Toplevel.name_of tr, the (Toplevel.source_of tr), tr));
 
 
 (** read theory **)
@@ -299,7 +299,7 @@
     val pos = Path.position path;
     val (name', parents, files) = ThyHeader.scan (src, pos);
     val ml_path = ThyLoad.ml_path name;
-    val ml_file = if ml andalso isSome (ThyLoad.check_file NONE ml_path) then [ml_path] else [];
+    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) ^
diff -r 8ac3803c8f73 -r 5fd94d84470f src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue May 17 10:19:43 2005 +0200
+++ b/src/Pure/Isar/proof.ML	Tue May 17 10:19:44 2005 +0200
@@ -793,7 +793,7 @@
     |> setup_goal I ProofContext.bind_propp_schematic_i ProofContext.fix_frees
       (Theorem {kind = kind,
         theory_spec = (a, map (snd o fst) concl),
-        locale_spec = (case raw_locale of NONE => NONE | SOME (_, x) => SOME (valOf opt_name, x)),
+        locale_spec = (case raw_locale of NONE => NONE | SOME (_, x) => SOME (the opt_name, x)),
         view = view,
         export = export})
       (AfterQed (Seq.single, after_global))
diff -r 8ac3803c8f73 -r 5fd94d84470f src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Tue May 17 10:19:43 2005 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Tue May 17 10:19:44 2005 +0200
@@ -73,7 +73,7 @@
 
 fun get thm =
   let
-    val n = getOpt (lookup_consumes thm, 0);
+    val n = if_none (lookup_consumes thm) 0;
     val ss =
       (case lookup_case_names thm of
         NONE => map Library.string_of_int (1 upto (Thm.nprems_of thm - n))
diff -r 8ac3803c8f73 -r 5fd94d84470f src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Tue May 17 10:19:43 2005 +0200
+++ b/src/Pure/Isar/session.ML	Tue May 17 10:19:44 2005 +0200
@@ -73,7 +73,7 @@
 
 fun get_rpath rpath_str =
   (if rpath_str = "" then () else
-     if isSome (!rpath) then
+     if is_some (! rpath) then
        error "Path for remote theory browsing information may only be set once"
      else
        rpath := SOME (Url.unpack rpath_str);
diff -r 8ac3803c8f73 -r 5fd94d84470f src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue May 17 10:19:43 2005 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue May 17 10:19:44 2005 +0200
@@ -201,7 +201,7 @@
 
 fun interruptible f x =
   let val y = ref (NONE: node History.T option);
-  in raise_interrupt (fn () => y := SOME (f x)) (); valOf (! y) end;
+  in raise_interrupt (fn () => y := SOME (f x)) (); the (! y) end;
 
 val rollback = ERROR_MESSAGE "Stale signature encountered after succesful execution!";
 
@@ -222,7 +222,7 @@
           (mk_state (transform_error (interruptible (trans f')) node), NONE)
             handle exn => (mk_state node, SOME exn);
       in
-        if is_stale result then return (mk_state node, SOME (getOpt (opt_exn, rollback)))
+        if is_stale result then return (mk_state node, SOME (if_none opt_exn rollback))
         else return (result, opt_exn)
       end;
 
diff -r 8ac3803c8f73 -r 5fd94d84470f src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Tue May 17 10:19:43 2005 +0200
+++ b/src/Pure/Syntax/ast.ML	Tue May 17 10:19:44 2005 +0200
@@ -210,7 +210,7 @@
     val changes = ref 0;
 
     fun subst _ (ast as Constant _) = ast
-      | subst env (Variable x) = valOf (Symtab.lookup (env, x))
+      | subst env (Variable x) = the (Symtab.lookup (env, x))
       | subst env (Appl asts) = Appl (map (subst env) asts);
 
     fun try_rules ((lhs, rhs) :: pats) ast =
diff -r 8ac3803c8f73 -r 5fd94d84470f src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Tue May 17 10:19:43 2005 +0200
+++ b/src/Pure/Syntax/printer.ML	Tue May 17 10:19:44 2005 +0200
@@ -186,14 +186,8 @@
 
 type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
 
-
-(*find tab for mode*)
-fun get_tab prtabs mode =
-  getOpt (assoc (prtabs, mode), Symtab.empty);
-
-(*collect tabs for mode hierarchy (default "")*)
-fun tabs_of prtabs modes =
-  List.mapPartial (fn mode => assoc (prtabs, mode)) (modes @ [""]);
+fun mode_tab prtabs mode = if_none (assoc (prtabs, mode)) Symtab.empty;
+fun mode_tabs prtabs modes = List.mapPartial (curry assoc prtabs) (modes @ [""]);
 
 
 (* xprod_to_fmt *)
@@ -246,7 +240,7 @@
 fun change_prtabs f mode xprods prtabs =
   let
     val fmts = List.mapPartial xprod_to_fmt xprods;
-    val tab = fold f fmts (get_tab prtabs mode);
+    val tab = fold f fmts (mode_tab prtabs mode);
   in overwrite (prtabs, (mode, tab)) end;
 
 fun extend_prtabs m = change_prtabs (curry Symtab.update_multi) m;
@@ -255,7 +249,7 @@
 fun merge_prtabs prtabs1 prtabs2 =
   let
     val modes = distinct (map fst (prtabs1 @ prtabs2));
-    fun merge m = (m, Symtab.merge_multi' (op =) (get_tab prtabs1 m, get_tab prtabs2 m));
+    fun merge m = (m, Symtab.merge_multi' (op =) (mode_tab prtabs1 m, mode_tab prtabs2 m));
   in map merge modes end;
 
 
@@ -358,14 +352,14 @@
 (* pretty_term_ast *)
 
 fun pretty_term_ast curried prtabs trf tokentrf ast =
-  Pretty.blk (0, pretty (tabs_of prtabs (! print_mode))
+  Pretty.blk (0, pretty (mode_tabs prtabs (! print_mode))
     trf tokentrf false curried ast 0);
 
 
 (* pretty_typ_ast *)
 
 fun pretty_typ_ast _ prtabs trf tokentrf ast =
-  Pretty.blk (0, pretty (tabs_of prtabs (! print_mode))
+  Pretty.blk (0, pretty (mode_tabs prtabs (! print_mode))
     trf tokentrf true false ast 0);
 
 end;
diff -r 8ac3803c8f73 -r 5fd94d84470f src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Tue May 17 10:19:43 2005 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Tue May 17 10:19:44 2005 +0200
@@ -216,7 +216,7 @@
     $$ "'" -- Scan.one Symbol.is_blank >> K NONE;
 
   val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (Scan.one (not_equal "'"));
-  val read_symbs = List.mapPartial I o valOf o Scan.read Symbol.stopper scan_symbs;
+  val read_symbs = List.mapPartial I o the o Scan.read Symbol.stopper scan_symbs;
 
   fun unique_index xsymbs =
     if length (List.filter is_index xsymbs) <= 1 then xsymbs
diff -r 8ac3803c8f73 -r 5fd94d84470f src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue May 17 10:19:43 2005 +0200
+++ b/src/Pure/axclass.ML	Tue May 17 10:19:44 2005 +0200
@@ -415,7 +415,7 @@
 
 fun prove mk_prop str_of sign prop thms usr_tac =
   (Tactic.prove sign [] [] (mk_prop prop)
-      (K (axclass_tac thms THEN (getOpt (usr_tac, all_tac))))
+      (K (axclass_tac thms THEN (if_none usr_tac all_tac)))
     handle ERROR => error ("The error(s) above occurred while trying to prove " ^
      quote (str_of sign prop))) |> Drule.standard;