--- a/src/HOL/Import/HOLLight/HOLLight.thy Wed Aug 31 13:28:29 2011 -0700
+++ b/src/HOL/Import/HOLLight/HOLLight.thy Thu Sep 01 16:16:25 2011 +0900
@@ -759,12 +759,12 @@
==> EX f::nat => 'A. ALL x::nat. f x = H f x"
by (import hollight WF_REC_num)
-lemma WF_MEASURE: "wfP (%(a::'A) b::'A. measure (m::'A => nat) (a, b))"
+lemma WF_MEASURE: "wfP (%(a::'A) b::'A. (a, b) : measure (m::'A => nat))"
by (import hollight WF_MEASURE)
lemma MEASURE_LE: "(ALL x::'q_12099.
- measure (m::'q_12099 => nat) (x, a::'q_12099) -->
- measure m (x, b::'q_12099)) =
+ (x, a::'q_12099) : measure (m::'q_12099 => nat) -->
+ (x, b::'q_12099) : measure m) =
(m a <= m b)"
by (import hollight MEASURE_LE)