src/Pure/Isar/obtain.ML

     fun occs_var x = Library.get_first (fn t =>
       ProofContext.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
     val raw_parms = map occs_var xs;
     val parms = mapfilter I raw_parms;
     val parm_names =
-      mapfilter (fn (Some (Free a), x) => Some (a, x) | _ => None) (raw_parms ~~ xs);
+      mapfilter (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (raw_parms ~~ xs);
 
     val that_prop =
       Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, bound_thesis))
       |> Library.curry Logic.list_rename_params (map #2 parm_names);
     val obtain_prop =
       Logic.list_rename_params ([AutoBind.thesisN],
         Term.list_all_free ([bound_thesis_var], Logic.mk_implies (that_prop, bound_thesis)));
 
     fun after_qed st = st
-      |> Method.local_qed false None print
+      |> Method.local_qed false NONE print
       |> Seq.map (fn st' => st'
         |> Proof.fix_i vars
         |> Proof.assm_i (export_obtain state parms (Proof.the_fact st')) asms);
   in
     state
     |> Proof.enter_forward
     |> Proof.have_i Seq.single true [(("", []), [(obtain_prop, ([], []))])]
-    |> Method.proof (Some (Method.Basic (K Method.succeed))) |> Seq.hd
-    |> Proof.fix_i [([thesisN], None)]
-    |> Proof.assume_i [((thatN, [ContextRules.intro_query_local None]), [(that_prop, ([], []))])]
+    |> Method.proof (SOME (Method.Basic (K Method.succeed))) |> Seq.hd
+    |> Proof.fix_i [([thesisN], NONE)]
+    |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])]
     |> (fn state' =>
         state'
         |> Proof.from_facts chain_facts
         |> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false
         |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))