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 |> |