Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more general dummy: may contain "parked arguments", for example;
authorwenzelm
Mon, 18 Aug 2014 15:46:27 +0200
changeset 58001 934d85f14d1d
parent 57982 d2bc61d78370
child 58002 0ed1e999a0fb
more general dummy: may contain "parked arguments", for example;
src/Pure/more_thm.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle