| changeset 45156 | a9b6c2ea7bec |
| parent 44117 | 88a5a8f44d15 |
| child 45347 | 66566a5df4be |
--- a/src/Pure/drule.ML Sun Oct 16 16:56:01 2011 +0200 +++ b/src/Pure/drule.ML Sun Oct 16 18:48:30 2011 +0200 @@ -729,7 +729,7 @@ fun cterm_rule f = dest_term o f o mk_term; fun term_rule thy f t = Thm.term_of (cterm_rule f (Thm.cterm_of thy t)); -val dummy_thm = mk_term (certify (Term.dummy_pattern propT)); +val dummy_thm = mk_term (certify Term.dummy_prop); (* sort_constraint *)