src/HOL/Tools/Nitpick/nitpick_nut.ML
changeset 38126 8031d099379a
parent 37678 0040bafffdef
child 38170 d74b66ec02ce
equal deleted inserted replaced
38125:b178a63df952 38126:8031d099379a
   719     val v = ConstName (s', T', R')
   719     val v = ConstName (s', T', R')
   720   in (v :: vs, NameTable.update (v, R') table) end
   720   in (v :: vs, NameTable.update (v, R') table) end
   721 fun choose_rep_for_sels_for_constr scope (x as (_, T)) =
   721 fun choose_rep_for_sels_for_constr scope (x as (_, T)) =
   722   fold_rev (choose_rep_for_nth_sel_for_constr scope x)
   722   fold_rev (choose_rep_for_nth_sel_for_constr scope x)
   723            (~1 upto num_sels_for_constr_type T - 1)
   723            (~1 upto num_sels_for_constr_type T - 1)
   724 fun choose_rep_for_sels_of_datatype _ ({deep = false, ...} : dtype_spec) = I
   724 fun choose_rep_for_sels_of_datatype _ ({deep = false, ...} : datatype_spec) = I
   725   | choose_rep_for_sels_of_datatype scope {constrs, ...} =
   725   | choose_rep_for_sels_of_datatype scope {constrs, ...} =
   726     fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
   726     fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
   727 fun choose_reps_for_all_sels (scope as {datatypes, ...}) =
   727 fun choose_reps_for_all_sels (scope as {datatypes, ...}) =
   728   fold (choose_rep_for_sels_of_datatype scope) datatypes o pair []
   728   fold (choose_rep_for_sels_of_datatype scope) datatypes o pair []
   729 
   729