# HG changeset patch
# User wenzelm
# Date 1408369587 -7200
# Node ID 934d85f14d1db25903699a231a465691d60a5405
# Parent  d2bc61d7837048a02fbecb056464d7e2dab9a56c
more general dummy: may contain "parked arguments", for example;

diff -r d2bc61d78370 -r 934d85f14d1d src/Pure/more_thm.ML
--- 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