# HG changeset patch
# User wenzelm
# Date 1116408659 -7200
# Node ID e0557c4521386be2638a4167b5bf8e87c3f492e0
# Parent  554836ed1f1b0be6e74323808e8745db427841c7
tuned;

diff -r 554836ed1f1b -r e0557c452138 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Wed May 18 11:30:58 2005 +0200
+++ b/src/Pure/General/file.ML	Wed May 18 11:30:59 2005 +0200
@@ -96,7 +96,7 @@
     | s => SOME (Info s))
   end;
 
-val exists = isSome o info;
+val exists = is_some o info;
 
 
 (* directories *)
diff -r 554836ed1f1b -r e0557c452138 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed May 18 11:30:58 2005 +0200
+++ b/src/Pure/General/name_space.ML	Wed May 18 11:30:59 2005 +0200
@@ -76,7 +76,7 @@
 (* basic operations *)
 
 fun map_space f xname tab =
-  Symtab.update ((xname, f (getOpt (Symtab.lookup (tab, xname), ([], [])))), tab);
+  Symtab.update ((xname, f (if_none (Symtab.lookup (tab, xname)) ([], []))), tab);
 
 fun change f xname (name, tab) =
   map_space (fn (names, names') => (f names name, names')) xname tab;
diff -r 554836ed1f1b -r e0557c452138 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Wed May 18 11:30:58 2005 +0200
+++ b/src/Pure/General/scan.ML	Wed May 18 11:30:59 2005 +0200
@@ -274,7 +274,7 @@
 
 fun drain def_prmpt get stopper scan ((state, xs), src) =
   (scan (state, xs), src) handle MORE prmpt =>
-    (case get (getOpt (prmpt, def_prmpt)) src of
+    (case get (if_none prmpt def_prmpt) src of
       ([], _) => (finite' stopper scan (state, xs), src)
     | (xs', src') => drain def_prmpt get stopper scan ((state, xs @ xs'), src'));
 
@@ -284,7 +284,7 @@
 
     fun drain_loop recover inp =
       drain_with (catch scanner) inp handle FAIL msg =>
-        (error_msg (getOpt (msg, "Syntax error.")); drain_with recover inp);
+        (error_msg (if_none msg "Syntax error."); drain_with recover inp);
 
     val ((ys, (state', xs')), src') =
       (case (get def_prmpt src, opt_recover) of
diff -r 554836ed1f1b -r e0557c452138 src/Pure/General/seq.ML
--- a/src/Pure/General/seq.ML	Wed May 18 11:30:58 2005 +0200
+++ b/src/Pure/General/seq.ML	Wed May 18 11:30:59 2005 +0200
@@ -71,8 +71,8 @@
 fun single x = cons (x, empty);
 
 (*head and tail -- beware of calling the sequence function twice!!*)
-fun hd xq = #1 (valOf (pull xq))
-and tl xq = #2 (valOf (pull xq));
+fun hd xq = #1 (the (pull xq))
+and tl xq = #2 (the (pull xq));
 
 (*partial function as procedure*)
 fun try f x =
diff -r 554836ed1f1b -r e0557c452138 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Wed May 18 11:30:58 2005 +0200
+++ b/src/Pure/General/symbol.ML	Wed May 18 11:30:59 2005 +0200
@@ -342,7 +342,7 @@
     else if is_ascii_quasi s then Quasi
     else if is_ascii_blank s then Blank
     else if is_char s then Other
-    else getOpt (Symtab.lookup (symbol_kinds, s), Other);
+    else if_none (Symtab.lookup (symbol_kinds, s)) Other;
 end;
 
 fun is_letter s = kind s = Letter;
@@ -417,7 +417,7 @@
 fun sym_explode str =
   let val chs = explode str in
     if no_explode chs then chs
-    else valOf (Scan.read stopper (Scan.repeat scan) chs)
+    else the (Scan.read stopper (Scan.repeat scan) chs)
   end;
 
 val chars_only = not o exists_string (equal "\\");
diff -r 554836ed1f1b -r e0557c452138 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Wed May 18 11:30:58 2005 +0200
+++ b/src/Pure/General/table.ML	Wed May 18 11:30:59 2005 +0200
@@ -95,12 +95,12 @@
 fun exists P tab = foldl_table (fn (false, e) => P e | (b, _) => b) (false, tab);
 
 fun min_key Empty = NONE
-  | min_key (Branch2 (left, (k, _), _)) = SOME (getOpt (min_key left, k))
-  | min_key (Branch3 (left, (k, _), _, _, _)) = SOME (getOpt (min_key left, k));
+  | min_key (Branch2 (left, (k, _), _)) = SOME (if_none (min_key left) k)
+  | min_key (Branch3 (left, (k, _), _, _, _)) = SOME (if_none (min_key left) k);
 
 fun max_key Empty = NONE
-  | max_key (Branch2 (_, (k, _), right)) = SOME (getOpt (max_key right, k))
-  | max_key (Branch3 (_, _, _, (k,_), right)) = SOME (getOpt (max_key right, k));
+  | max_key (Branch2 (_, (k, _), right)) = SOME (if_none (max_key right) k)
+  | max_key (Branch3 (_, _, _, (k,_), right)) = SOME (if_none (max_key right) k);
 
 
 (* lookup *)
@@ -184,7 +184,7 @@
 fun extend (table, args) =
   let
     fun add (key, x) (tab, dups) =
-      if isSome (lookup (tab, key)) then (tab, key :: dups)
+      if is_some (lookup (tab, key)) then (tab, key :: dups)
       else (update ((key, x), tab), dups);
   in
     (case fold add args (table, []) of
@@ -212,12 +212,12 @@
   | del NONE (Branch3 (Empty, p, Empty, q, Empty)) =
       (p, (false, Branch2 (Empty, q, Empty)))
   | del k (Branch2 (Empty, p, Empty)) = (case compare k p of
-      EQUAL => (p, (true, Empty)) | _ => raise UNDEF (valOf k))
+      EQUAL => (p, (true, Empty)) | _ => raise UNDEF (the k))
   | del k (Branch3 (Empty, p, Empty, q, Empty)) = (case compare k p of
       EQUAL => (p, (false, Branch2 (Empty, q, Empty)))
     | _ => (case compare k q of
         EQUAL => (q, (false, Branch2 (Empty, p, Empty)))
-      | _ => raise UNDEF (valOf k)))
+      | _ => raise UNDEF (the k)))
   | del k (Branch2 (l, p, r)) = (case compare k p of
       LESS => (case del k l of
         (p', (false, l')) => (p', (false, Branch2 (l', p, r)))
@@ -311,7 +311,7 @@
 
 (* tables with multiple entries per key *)
 
-fun lookup_multi arg = getOpt (lookup arg, []);
+fun lookup_multi arg = if_none (lookup arg) [];
 
 fun update_multi ((key, x), tab) = modify key (fn NONE => [x] | SOME xs => x :: xs) tab;
 
diff -r 554836ed1f1b -r e0557c452138 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Wed May 18 11:30:58 2005 +0200
+++ b/src/Pure/Isar/isar_output.ML	Wed May 18 11:30:59 2005 +0200
@@ -1,6 +1,6 @@
 (*  Title:      Pure/Isar/isar_output.ML
     ID:         $Id$
-    Author:     Florian Haftmann, TU Muenchen
+    Author:     Markus Wenzel, TU Muenchen
 
 Isar theory output.
 *)
@@ -310,6 +310,7 @@
   ("source", Library.setmp source o boolean),
   ("goals_limit", Library.setmp goals_limit o integer)];
 
+
 (* commands *)
 
 fun cond_quote prt =
@@ -345,23 +346,17 @@
 
 fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt;
 
-fun pretty_term_typ_old ctxt term = Pretty.block [
-  ((ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt) term),
-  (Pretty.str "\\<Colon>") (* q'n'd *),
-  ((ProofContext.pretty_typ ctxt o Term.type_of o ProofContext.extern_skolem ctxt) term)
-  ]
+fun pretty_term_typ ctxt t =
+  (Syntax.const Syntax.constrainC $
+    ProofContext.extern_skolem ctxt t $
+    Syntax.term_of_typ (! show_sorts) (Term.fastype_of t))
+  |> ProofContext.pretty_term ctxt;
 
-fun pretty_term_typ ctxt term = let val t = (ProofContext.extern_skolem ctxt term) in
-  ProofContext.pretty_term ctxt (
-    Syntax.const Syntax.constrainC $ t $ Syntax.term_of_typ (!show_sorts) (fastype_of t)
-  )
-end;
+fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of;
 
-fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of o ProofContext.extern_skolem ctxt;
-
-fun pretty_term_const ctxt (Const c) = pretty_term ctxt (Const c)
-  | pretty_term_const ctxt term =
-      raise (Output.ERROR_MESSAGE ("Not a defined constant: " ^ (Term.string_of_term term)))
+fun pretty_term_const ctxt t =
+  if Term.is_Const t then pretty_term ctxt t
+  else error ("Logical constant expected: " ^ ProofContext.string_of_term ctxt t);
 
 fun pretty_thm ctxt = pretty_term ctxt o Thm.prop_of;