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