src/Tools/quickcheck.ML
changeset 30473 e0b66c11e7e4
parent 29266 4a478f9d2847
child 30824 bc6b24882834
equal deleted inserted replaced
30472:9dea0866021c 30473:e0b66c11e7e4
   142 val auto_time_limit = ref 5000;
   142 val auto_time_limit = ref 5000;
   143 
   143 
   144 fun test_goal_auto int state =
   144 fun test_goal_auto int state =
   145   let
   145   let
   146     val ctxt = Proof.context_of state;
   146     val ctxt = Proof.context_of state;
   147     val assms = map term_of (Assumption.assms_of ctxt);
   147     val assms = map term_of (Assumption.all_assms_of ctxt);
   148     val Test_Params { size, iterations, default_type } =
   148     val Test_Params { size, iterations, default_type } =
   149       (snd o Data.get o Proof.theory_of) state;
   149       (snd o Data.get o Proof.theory_of) state;
   150     fun test () =
   150     fun test () =
   151       let
   151       let
   152         val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_time_limit))
   152         val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_time_limit))