src/HOL/Tools/SMT/z3_proof_tools.ML

--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Mar 09 10:28:01 2011 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Mar 09 21:40:38 2011 +0100
@@ -177,7 +177,8 @@
   let val (cv, cu) = Thm.dest_abs NONE ct
   in f (cv :: cvs) cu #>> Thm.cabs cv end
 
-val is_atomic = (fn _ $ _ => false | Abs _ => false | _ => true)
+val is_atomic =
+  (fn Free _ => true | Var _ => true | Bound _ => true | _ => false)
 
 fun abstract (ext_logic, with_theories) =
   let