src/Pure/more_thm.ML
changeset 58001 934d85f14d1d
parent 56245 84fc7dfa3cd4
child 59058 a78612c67ec0
--- a/src/Pure/more_thm.ML	Mon Aug 18 15:03:25 2014 +0200
+++ b/src/Pure/more_thm.ML	Mon Aug 18 15:46:27 2014 +0200
@@ -234,7 +234,7 @@
 fun is_dummy thm =
   (case try Logic.dest_term (Thm.concl_of thm) of
     NONE => false
-  | SOME t => Term.is_dummy_pattern t);
+  | SOME t => Term.is_dummy_pattern (Term.head_of t));
 
 fun plain_prop_of raw_thm =
   let