changeset 44058 | ae85c5d64913 |
parent 44025 | ec2a7901217b |
child 44921 | 58eef4843641 |
--- a/src/HOL/Orderings.thy Mon Aug 08 16:38:59 2011 +0200 +++ b/src/HOL/Orderings.thy Mon Aug 08 17:23:15 2011 +0200 @@ -531,7 +531,7 @@ setup {* let -fun prp t thm = (#prop (rep_thm thm) = t); +fun prp t thm = Thm.prop_of thm = t; (* FIXME aconv!? *) fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) = let val prems = Simplifier.prems_of ss;