src/ZF/Constructible/AC_in_L.thy

              X = {x\<in>A. sats(A, p, Cons(x,env))} &
              env_form_map(f,r,A,<env,p>) = k"
 
   DPow_least :: "[i,i,i,i]=>i"
     --{*function yielding the smallest index for @{term X}*}
-   "DPow_least(f,r,A,X) == \<mu>k. DPow_ord(f,r,A,X,k)"
+   "DPow_least(f,r,A,X) == \<mu> k. DPow_ord(f,r,A,X,k)"
 
   DPow_r :: "[i,i,i]=>i"
     --{*a wellordering on @{term "DPow(A)"}*}
    "DPow_r(f,r,A) == measure(DPow(A), DPow_least(f,r,A))"