src/HOL/Orderings.thy

--- 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;