src/HOL/Tools/function_package/lexicographic_order.ML
changeset 30304 d8e4cd2ac2a1
parent 29713 55c30d1117ef
child 30493 b8570ea1ce25
equal deleted inserted replaced
30303:9c4f4ac0d038 30304:d8e4cd2ac2a1
    22 
    22 
    23 fun mk_measures domT mfuns =
    23 fun mk_measures domT mfuns =
    24     let 
    24     let 
    25         val relT = HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))
    25         val relT = HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))
    26         val mlexT = (domT --> HOLogic.natT) --> relT --> relT
    26         val mlexT = (domT --> HOLogic.natT) --> relT --> relT
    27         fun mk_ms [] = Const (@{const_name "{}"}, relT)
    27         fun mk_ms [] = Const (@{const_name Set.empty}, relT)
    28           | mk_ms (f::fs) = 
    28           | mk_ms (f::fs) = 
    29             Const (@{const_name "mlex_prod"}, mlexT) $ f $ mk_ms fs
    29             Const (@{const_name "mlex_prod"}, mlexT) $ f $ mk_ms fs
    30     in
    30     in
    31         mk_ms mfuns
    31         mk_ms mfuns
    32     end
    32     end