src/Tools/quickcheck.ML

     val {goal = st, ...} = Proof.raw_goal state;
     val (gi, frees) = Logic.goal_params (prop_of st) i;
     val gi' = Logic.list_implies (if no_assms then [] else assms,
                                   subst_bounds (frees, strip gi))
       |> monomorphic_term thy insts default_T
-      |> ObjectLogic.atomize_term thy;
+      |> Object_Logic.atomize_term thy;
   in gen_test_term ctxt quiet report generator_name size iterations gi' end;
 
 fun pretty_counterex ctxt NONE = Pretty.str "Quickcheck found no counterexample."
   | pretty_counterex ctxt (SOME cex) =
       Pretty.chunks (Pretty.str "Quickcheck found a counterexample:\n" ::