equal
deleted
inserted
replaced
223 fun define_raw_fv dt_info bns bmlll lthy = |
223 fun define_raw_fv dt_info bns bmlll lthy = |
224 let |
224 let |
225 val thy = ProofContext.theory_of lthy; |
225 val thy = ProofContext.theory_of lthy; |
226 val {descr, sorts, ...} = dt_info; |
226 val {descr, sorts, ...} = dt_info; |
227 |
227 |
228 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
228 val fv_names = prefix_dt_names descr sorts "fv_" |
229 "fv_" ^ Datatype_Aux.name_of_typ (nth_dtyp descr sorts i)) descr); |
|
230 |
229 |
231 val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) descr; |
230 val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) descr; |
232 val fv_frees = map Free (fv_names ~~ fv_types); |
231 val fv_frees = map Free (fv_names ~~ fv_types); |
233 val (bn_fvbn, (fv_bn_names, fv_bn_eqs)) = fv_bns thy dt_info fv_frees bns bmlll; |
232 val (bn_fvbn, (fv_bn_names, fv_bn_eqs)) = fv_bns thy dt_info fv_frees bns bmlll; |
234 |
233 |