src/HOL/Tools/record_package.ML
changeset 8246 efb3c8253d90
parent 8168 9d2ac5439089
child 8274 0d8fa545bd5c
equal deleted inserted replaced
8245:6acc80f7f36f 8246:efb3c8253d90
   825     (* 4th stage: final_thy *)
   825     (* 4th stage: final_thy *)
   826 
   826 
   827     val final_thy =
   827     val final_thy =
   828       thms_thy
   828       thms_thy
   829       |> put_record name {args = args, parent = parent, fields = fields, simps = simps}
   829       |> put_record name {args = args, parent = parent, fields = fields, simps = simps}
   830       |> put_sel_upd names (simps @ update_defs)
   830       |> put_sel_upd names (field_simps @ sel_defs @ update_defs)
   831       |> add_record_splits named_splits
   831       |> add_record_splits named_splits
   832       |> Theory.parent_path;
   832       |> Theory.parent_path;
   833 
   833 
   834   in (final_thy, {simps = simps, iffs = iffs}) end;
   834   in (final_thy, {simps = simps, iffs = iffs}) end;
   835 
   835