--- a/src/Tools/quickcheck.ML Fri Dec 03 08:40:47 2010 +0100
+++ b/src/Tools/quickcheck.ML Fri Dec 03 08:40:47 2010 +0100
@@ -220,15 +220,16 @@
fun test_goal_terms lthy is_interactive insts check_goals =
let
val thy = ProofContext.theory_of lthy
+ val default_insts =
+ if Config.get lthy finite_types then (get_finite_types lthy) else (default_type lthy)
val inst_goals =
- if Config.get lthy finite_types then
- maps (fn check_goal => map (fn T =>
- Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
- handle WELLSORTED s => Wellsorted_Error s) (get_finite_types lthy)) check_goals
- else
- maps (fn check_goal => map (fn T =>
- Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
- handle WELLSORTED s => Wellsorted_Error s) (default_type lthy)) check_goals
+ maps (fn check_goal =>
+ if not (null (Term.add_tfree_names check_goal [])) then
+ map (fn T =>
+ ((Term o Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
+ handle WELLSORTED s => Wellsorted_Error s) default_insts
+ else
+ [Term (Object_Logic.atomize_term thy check_goal)]) check_goals
val error_msg = cat_lines (map_filter (fn Term t => NONE | Wellsorted_Error s => SOME s) inst_goals)
val correct_inst_goals =
case map_filter (fn Term t => SOME t | Wellsorted_Error s => NONE) inst_goals of