173 

   174 text {*

   175   Unabs_def converts a definition given as

   176 

   177     c \<equiv> %x. %y. f x y

   178 

   179   to a theorem of the form

   180 

   181     c x y \<equiv> f x y

   182 

   183   This function is needed to rewrite the right-hand

   184   side to the left-hand side.

   185 *}

   186 

   187 ML {*

   188 fun unabs_def ctxt def =

   189 let

   190   val (lhs, rhs) = Thm.dest_equals (cprop_of def)

   191   val xs = strip_abs_vars (term_of rhs)

   192   val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt

   193 

   194   val thy = ProofContext.theory_of ctxt'

   195   val cxs = map (cterm_of thy o Free) xs

   196   val new_lhs = Drule.list_comb (lhs, cxs)

   197 

   198   fun get_conv [] = Conv.rewr_conv def

   199     | get_conv (x::xs) = Conv.fun_conv (get_conv xs)

   200 in

   201   get_conv xs new_lhs |>

   202   singleton (ProofContext.export ctxt' ctxt)

   203 end

   204 *}