tuned: concise combinators instead of bulky case-expressions;

--- a/src/Pure/Isar/bundle.ML	Sat Apr 22 20:55:05 2023 +0200
+++ b/src/Pure/Isar/bundle.ML	Sat Apr 22 21:00:24 2023 +0200
@@ -70,9 +70,8 @@
 (* target -- bundle under construction *)
 
 fun the_target thy =
-  (case #2 (Data.get (Context.Theory thy)) of
-    SOME thms => thms
-  | NONE => error "Missing bundle target");
+  #2 (Data.get (Context.Theory thy))
+  |> \<^if_none>\<open>error "Missing bundle target"\<close>;
 
 val reset_target = (Context.theory_map o Data.map o apsnd o K) NONE;
 val set_target = Context.theory_map o Data.map o apsnd o K o SOME o Attrib.trim_context_thms;

--- a/src/Pure/Isar/class.ML	Sat Apr 22 20:55:05 2023 +0200
+++ b/src/Pure/Isar/class.ML	Sat Apr 22 21:00:24 2023 +0200
@@ -121,9 +121,8 @@
   | NONE => NONE);
 
 fun the_class_data thy class =
-  (case lookup_class_data thy class of
-    NONE => error ("Undeclared class " ^ quote class)
-  | SOME data => data);
+  lookup_class_data thy class
+  |> \<^if_none>\<open>error ("Undeclared class " ^ quote class)\<close>;
 
 val is_class = is_some oo lookup_class_data;
 

--- a/src/Pure/Isar/context_rules.ML	Sat Apr 22 20:55:05 2023 +0200
+++ b/src/Pure/Isar/context_rules.ML	Sat Apr 22 21:00:24 2023 +0200
@@ -77,7 +77,7 @@
 
 fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) =
   let
-    val w = (case opt_w of SOME w => w | NONE => Tactic.subgoals_of_brl (b, th));
+    val w = opt_w |> \<^if_none>\<open>Tactic.subgoals_of_brl (b, th)\<close>;
     val th' = Thm.trim_context th;
   in
     make_rules (next - 1) ((w, ((i, b), th')) :: rules)

--- a/src/Pure/Isar/method.ML	Sat Apr 22 20:55:05 2023 +0200
+++ b/src/Pure/Isar/method.ML	Sat Apr 22 21:00:24 2023 +0200
@@ -321,9 +321,8 @@
 fun set_tactic ml_tactic = map_data (fn (methods, _, facts) => (methods, SOME ml_tactic, facts));
 
 fun the_tactic context =
-  (case #ml_tactic (Data.get context) of
-    SOME tac => tac
-  | NONE => raise Fail "Undefined ML tactic");
+  #ml_tactic (Data.get context)
+  |> \<^if_none>\<open>raise Fail "Undefined ML tactic"\<close>;
 
 val parse_tactic =
   Scan.state :|-- (fn context =>

--- a/src/Pure/Isar/obtain.ML	Sat Apr 22 20:55:05 2023 +0200
+++ b/src/Pure/Isar/obtain.ML	Sat Apr 22 21:00:24 2023 +0200
@@ -105,9 +105,8 @@
   let
     val frees = Frees.build (t |> Term.fold_aterms (fn Free v => Frees.add_set v | _ => I));
     val T =
-      (case Frees.get_first (fn ((x, T), _) => if x = z then SOME T else NONE) frees of
-        SOME T => T
-      | NONE => the_default dummyT (Variable.default_type ctxt z));
+      Frees.get_first (fn ((x, T), _) => if x = z then SOME T else NONE) frees
+      |> \<^if_none>\<open>the_default dummyT (Variable.default_type ctxt z)\<close>;
   in Logic.all_const T $ Term.lambda_name (y, Free (z, T)) t end;
 
 fun prepare_clause prep_var parse_prop mk_all ctxt thesis raw_vars raw_props =

--- a/src/Pure/Isar/proof.ML	Sat Apr 22 20:55:05 2023 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Apr 22 21:00:24 2023 +0200
@@ -355,9 +355,8 @@
     (ctxt, statement, using, goal, before_qed, after_qed));
 
 fun find_goal state =
-  (case try current_goal state of
-    SOME ctxt_goal => ctxt_goal
-  | NONE => find_goal (close_block state handle ERROR _ => error "No proof goal"));
+  try current_goal state
+  |> \<^if_none>\<open>find_goal (close_block state handle ERROR _ => error "No proof goal")\<close>;
 
 
 
@@ -1298,9 +1297,7 @@
 );
 
 fun the_result ctxt =
-  (case Result.get ctxt of
-    NONE => error "No result of forked proof"
-  | SOME th => th);
+  Result.get ctxt |> \<^if_none>\<open>error "No result of forked proof"\<close>;
 
 val set_result = Result.put o SOME;
 val reset_result = Result.put NONE;

--- a/src/Pure/Isar/proof_display.ML	Sat Apr 22 20:55:05 2023 +0200
+++ b/src/Pure/Isar/proof_display.ML	Sat Apr 22 21:00:24 2023 +0200
@@ -44,9 +44,8 @@
   (case Context.get_generic_context () of
     SOME (Context.Proof ctxt) => ctxt
   | SOME (Context.Theory thy) =>
-      (case try Syntax.init_pretty_global thy of
-        SOME ctxt => ctxt
-      | NONE => Syntax.init_pretty_global (mk_thy ()))
+      try Syntax.init_pretty_global thy
+      |> \<^if_none>\<open>Syntax.init_pretty_global (mk_thy ())\<close>
   | NONE => Syntax.init_pretty_global (mk_thy ()));
 
 fun pp_thm mk_thy th =

--- a/src/Pure/Isar/toplevel.ML	Sat Apr 22 20:55:05 2023 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Apr 22 21:00:24 2023 +0200
@@ -217,9 +217,8 @@
   |> Presentation_State.put (SOME (State (current, (NONE, NONE))));
 
 fun presentation_state ctxt =
-  (case Presentation_State.get ctxt of
-    NONE => State (node_presentation (Theory (Context.Proof ctxt)), (NONE, NONE))
-  | SOME state => state);
+  Presentation_State.get ctxt
+  |> \<^if_none>\<open>State (node_presentation (Theory (Context.Proof ctxt)), (NONE, NONE))\<close>;
 
 
 (* print state *)

--- a/src/Pure/axclass.ML	Sat Apr 22 20:55:05 2023 +0200
+++ b/src/Pure/axclass.ML	Sat Apr 22 21:00:24 2023 +0200
@@ -215,17 +215,14 @@
 (* declaration and definition of instances of overloaded constants *)
 
 fun inst_tyco_of thy (c, T) =
-  (case get_inst_tyco (Sign.consts_of thy) (c, T) of
-    SOME tyco => tyco
-  | NONE => error ("Illegal type for instantiation of class parameter: " ^
-      quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T)));
+  get_inst_tyco (Sign.consts_of thy) (c, T)
+  |> \<^if_none>\<open>
+    error ("Illegal type for instantiation of class parameter: " ^
+      quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T))\<close>;
 
 fun declare_overloaded (c, T) thy =
   let
-    val class =
-      (case class_of_param thy c of
-        SOME class => class
-      | NONE => error ("Not a class parameter: " ^ quote c));
+    val class = class_of_param thy c |> \<^if_none>\<open>error ("Not a class parameter: " ^ quote c)\<close>;
     val tyco = inst_tyco_of thy (c, T);
     val name_inst = instance_name (tyco, class) ^ "_inst";
     val c' = instance_name (tyco, c);

--- a/src/Pure/par_tactical.ML	Sat Apr 22 20:55:05 2023 +0200
+++ b/src/Pure/par_tactical.ML	Sat Apr 22 21:00:24 2023 +0200
@@ -59,10 +59,7 @@
     SOME goals =>
       if Future.relevant goals then
         let
-          fun try_goal g =
-            (case SINGLE tac (Goal.init g) of
-              NONE => raise FAILED ()
-            | SOME st' => st');
+          fun try_goal g = SINGLE tac (Goal.init g) |> \<^if_none>\<open>raise FAILED ()\<close>;
           val results = Par_List.map try_goal goals;
         in retrofit_tac {close = false} (rev results) st end handle FAILED () => Seq.empty
       else DETERM tac st