src/Tools/quickcheck.ML

               (v, ProofContext.read_typ ctxt arg)
         | _ => (apfst o parse_test_param ctxt) (name, arg);
 
 fun quickcheck_params_cmd args thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val f = fold (parse_test_param ctxt) args;
   in
     thy
     |> (Data.map o apsnd o map_test_params) f
   end;