# HG changeset patch
# User bulwahn
# Date 1322641278 -3600
# Node ID a07654c67f305a3d2f88b77ad130d78371d2bacb
# Parent  cf22004ad55d628f6a5a22d36fd8a061441cb598
quickcheck does not show evaluation terms of equations if they are simply free variables to avoid duplicated output; tuned

diff -r cf22004ad55d -r a07654c67f30 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Nov 30 09:21:15 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Nov 30 09:21:18 2011 +0100
@@ -276,13 +276,13 @@
         collect_results f ts (result :: results)
     end  
 
-fun add_equation_eval_terms (t, eval_terms) =
-  case try HOLogic.dest_eq (snd (strip_imp t)) of
-    SOME (lhs, rhs) => (t, eval_terms @ [rhs, lhs])
-  | NONE => (t, eval_terms)
-
 fun generator_test_goal_terms (name, compile) ctxt catch_code_errors insts goals =
   let
+    fun add_eval_term t ts = if is_Free t then ts else ts @ [t]
+    fun add_equation_eval_terms (t, eval_terms) =
+      case try HOLogic.dest_eq (snd (strip_imp t)) of
+        SOME (lhs, rhs) => (t, add_eval_term lhs (add_eval_term rhs eval_terms))
+      | NONE => (t, eval_terms)
     fun test_term' goal =
       case goal of
         [(NONE, t)] => test_term (name, compile) ctxt catch_code_errors t