75 *}

    75 *}

    76 

    76 

    77 ML {*

    77 ML {*

    78 fun setify x =

    78 fun setify x =

    79   if fastype_of x = @{typ "atom list"} 

    79   if fastype_of x = @{typ "atom list"} 

    82 *}

    82 *}

    83 

    83 

    84 ML {*

    84 ML {*

    85 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys =

    85 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys =

    86 let

    86 let

   129 | BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y

   129 | BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y

   130 | BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y

   130 | BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y

   131 *}

   131 *}

   132 

   132 

   133 ML {*

   133 ML {*

   136 let

   135 let

   137   fun fv_bn_constr (cname, dts) (args_in_bn, bml) =

   136   fun fv_bn_constr (cname, dts) (args_in_bn, bml) =

   138   let

   137   let

   139     val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;

   138     val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;

   140     val names = Datatype_Prop.make_tnames Ts;

   139     val names = Datatype_Prop.make_tnames Ts;

   216   Function.termination_proof NONE

   215   Function.termination_proof NONE

   217   #> Proof.global_terminal_proof (Method.Basic method, NONE)

   216   #> Proof.global_terminal_proof (Method.Basic method, NONE)

   218 *}

   217 *}

   219 

   218 

   220 ML {*

   219 ML {*

   222 let

   221 let

   223   val thy = ProofContext.theory_of lthy;

   222   val thy = ProofContext.theory_of lthy;

   224   val {descr as dt_descr, sorts, ...} = dt_info;

   223   val {descr as dt_descr, sorts, ...} = dt_info;

   225 

   224 

   226   val fv_names = prefix_dt_names dt_descr sorts "fv_"

   225   val fv_names = prefix_dt_names dt_descr sorts "fv_"