# HG changeset patch
# User bulwahn
# Date 1291362047 -3600
# Node ID c600f6ae4b09f3bd67f4924a31e981420c621e20
# Parent  7abeb749ae99f45c04076eac606baaa68b5dd28d
only instantiate type variable if there exists some in quickcheck

diff -r 7abeb749ae99 -r c600f6ae4b09 src/Tools/quickcheck.ML
--- 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