src/Tools/quickcheck.ML
changeset 31138 a51ce445d498
parent 30980 fe0855471964
child 31153 6b31b143f18b
equal deleted inserted replaced
31137:cd3aafc1c631 31138:a51ce445d498
    92   let
    92   let
    93     val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
    93     val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
    94       error "Term to be tested contains type variables";
    94       error "Term to be tested contains type variables";
    95     val _ = null (Term.add_vars t []) orelse
    95     val _ = null (Term.add_vars t []) orelse
    96       error "Term to be tested contains schematic variables";
    96       error "Term to be tested contains schematic variables";
    97     val frees = map dest_Free (OldTerm.term_frees t);
    97     val frees = Term.add_frees t [];
    98   in (map fst frees, list_abs_free (frees, t)) end
    98   in (map fst frees, list_abs_free (frees, t)) end
    99 
    99 
   100 fun test_term ctxt quiet generator_name size i t =
   100 fun test_term ctxt quiet generator_name size i t =
   101   let
   101   let
   102     val (names, t') = prep_test_term t;
   102     val (names, t') = prep_test_term t;