src/HOL/Tools/datatype_rep_proofs.ML
changeset 28084 a05ca48ef263
parent 28083 103d9282a946
child 28362 b0ebac91c8d5
equal deleted inserted replaced
28083:103d9282a946 28084:a05ca48ef263
   185         InductivePackage.add_inductive_global (serial_string ())
   185         InductivePackage.add_inductive_global (serial_string ())
   186           {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
   186           {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
   187            alt_name = Name.binding big_rec_name, coind = false, no_elim = true, no_ind = false,
   187            alt_name = Name.binding big_rec_name, coind = false, no_elim = true, no_ind = false,
   188            skip_mono = true}
   188            skip_mono = true}
   189           (map (fn s => ((Name.binding s, UnivT'), NoSyn)) rep_set_names') []
   189           (map (fn s => ((Name.binding s, UnivT'), NoSyn)) rep_set_names') []
   190           (map (fn x => ((Name.no_binding, []), x)) intr_ts) [] thy1;
   190           (map (fn x => (Attrib.no_binding, x)) intr_ts) [] thy1;
   191 
   191 
   192     (********************************* typedef ********************************)
   192     (********************************* typedef ********************************)
   193 
   193 
   194     val (typedefs, thy3) = thy2 |>
   194     val (typedefs, thy3) = thy2 |>
   195       parent_path flat_names |>
   195       parent_path flat_names |>