src/Pure/Isar/proof_context.ML

 (*  Title:      Pure/Isar/proof_context.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
-                contributions by Rafal Kolanski, NICTA
 
 The key concept of Isar proof contexts.
 *)
 
 val show_structs = ref false;

 
 fun fixes_of (Context {asms = (_, fixes), ...}) = fixes;
 val fixed_names_of = map #2 o fixes_of;
 fun is_fixed ctxt x = exists (equal x o #2) (fixes_of ctxt);
 fun is_known (ctxt as Context {defs = (types, _, _, _), ...}) x =
-  isSome (Vartab.lookup (types, (x, ~1))) orelse is_fixed ctxt x;
+  is_some (Vartab.lookup (types, (x, ~1))) orelse is_fixed ctxt x;
 fun type_occs (Context {defs = (_, _, _, tab), ...}) = tab;
 
 fun assumptions_of (Context {asms = ((asms, _), _), ...}) = asms;
 fun prems_of (Context {asms = ((_, prems), _), ...}) = List.concat (map #2 prems);
 

 
 
 (* internalize Skolem constants *)
 
 fun lookup_skolem ctxt x = assoc (fixes_of ctxt, x);
-fun get_skolem ctxt x = getOpt (lookup_skolem ctxt x, x);
+fun get_skolem ctxt x = if_none (lookup_skolem ctxt x) x;
 
 fun no_skolem internal ctxt x =
   if can Syntax.dest_skolem x then
     raise CONTEXT ("Illegal reference to internal Skolem constant: " ^ quote x, ctxt)
   else if not internal andalso can Syntax.dest_internal x then

 
 (* type and constant names *)
 
 fun read_tyname ctxt c =
   if c mem_string used_types ctxt then
-    TFree (c, getOpt (def_sort ctxt (c, ~1), Sign.defaultS (sign_of ctxt)))
+    TFree (c, if_none (def_sort ctxt (c, ~1)) (Sign.defaultS (sign_of ctxt)))
   else Sign.read_tyname (sign_of ctxt) c;
 
 fun read_const ctxt c =
   (case lookup_skolem ctxt c of
     SOME c' => Free (c', dummyT)

     fun still_fixed (Free (x, _)) = not (x mem_string extra_fixes)
       | still_fixed _ = false;
     val occs_inner = type_occs inner;
     val occs_outer = type_occs outer;
     fun add (gen, a) =
-      if isSome (Symtab.lookup (occs_outer, a)) orelse
+      if is_some (Symtab.lookup (occs_outer, a)) orelse
         exists still_fixed (Symtab.lookup_multi (occs_inner, a))
       then gen else a :: gen;
   in fn tfrees => Library.foldl add ([], tfrees) end;
 
 fun generalize inner outer ts =

     val _ = if liberal then () else
       (case List.filter (not o Syntax.is_identifier) (map (no_skolem internal ctxt) xs) of
       [] => () | bads => raise CONTEXT ("Bad variable name(s): " ^ commas_quote bads, ctxt));
 
     val opt_T = Option.map (cond_tvars o prep_typ ctxt) raw_T;
-    val T = getOpt (opt_T, TypeInfer.logicT);
+    val T = if_none opt_T TypeInfer.logicT;
     val ctxt' = ctxt |> declare_terms_syntax (map (fn x => Free (x, T)) xs);
   in (ctxt', (xs, opt_T)) end;
 
 in
 

 
 (** cases **)
 
 fun prep_case ctxt name xs {fixes, assumes, binds} =
   let
-    fun replace (opt_x :: xs) ((y, T) :: ys) = (getOpt (opt_x,y), T) :: replace xs ys
+    fun replace (opt_x :: xs) ((y, T) :: ys) = (if_none opt_x y, T) :: replace xs ys
       | replace [] ys = ys
       | replace (_ :: _) [] = raise CONTEXT ("Too many parameters for case " ^ quote name, ctxt);
   in
     if null (foldr Term.add_typ_tvars [] (map snd fixes)) andalso
       null (foldr Term.add_term_vars [] (List.concat (map snd assumes))) then

     val matches2 = PureThy.find_theorems facts2 filters2;
     
     (* combine them, use a limit, then print *)
     val matches = matches1 @ matches2;
     val len = length matches;
-    val limit = getOpt (opt_limit, ! thms_containing_limit);
+    val limit = if_none opt_limit (! thms_containing_limit);
     val count = Int.min (limit, len);
     
     val header = Pretty.blk (0, [Pretty.str "Searched for:", Pretty.fbrk,
             Pretty.indent 4 (
                 Pretty.blk (0, separate Pretty.fbrk (map Pretty.str ss))),