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