src/Pure/codegen.ML

     fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
       | strip t = t;
     val (gi, frees) = Logic.goal_params
       (prop_of (snd (snd (Proof.get_goal (Toplevel.proof_of st))))) i;
     val gi' = ObjectLogic.atomize_term thy (map_term_types
-      (map_type_tfree (fn p as (s, _) => getOpt (AList.lookup (op =) tvinsts s,
-        getOpt (default_type, TFree p)))) (subst_bounds (frees, strip gi)));
+      (map_type_tfree (fn p as (s, _) =>
+        the_default (the_default (TFree p) default_type)
+          (AList.lookup (op =) tvinsts s))) (subst_bounds (frees, strip gi)));
   in case test_term (Toplevel.theory_of st) size iterations gi' of
       NONE => writeln "No counterexamples found."
     | SOME cex => writeln ("Counterexample found:\n" ^
         Pretty.string_of (Pretty.chunks (map (fn (s, t) =>
           Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1,

   OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag
   (Scan.option (P.$$$ "[" |-- P.list1
     (   parse_test_params >> (fn f => fn thy => apfst (f thy))
      || parse_tyinst) --| P.$$$ "]") -- Scan.optional P.nat 1 >>
     (fn (ps, g) => Toplevel.keep (fn st =>
-      test_goal (app (getOpt (Option.map
-          (map (fn f => f (Toplevel.theory_of st))) ps, []))
+      test_goal (app (the_default [] (Option.map (map (fn f => f (Toplevel.theory_of st))) ps))
         (get_test_params (Toplevel.theory_of st), [])) g st)));
 
 val valueP =
   OuterSyntax.improper_command "value" "read, evaluate and print term" K.diag
     (P.term >> (Toplevel.no_timing oo print_evaluated_term));