--- 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 =